The area formula for injective maps with injective derivative

Let U and V be finite-dimensional real inner product spaces, m = dim U, and let f : U → V be injective on a measurable set s, differentiable at every point of s with injective derivative. This file proves the area formula

∫⁻ x in s, J f x = μHE[m] (f '' s),

where J f x = (fderiv ℝ f x).normDet is the m-dimensional Jacobian (LinearMap.normDet) and μHE[m] is the m-dimensional Euclidean Hausdorff measure on V, normalized to agree with Lebesgue measure on m-dimensional subspaces. For V = U, where normDet is |det| and μHE[m] is the volume, this is the case of Mathlib's change of variables formula MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image with invertible derivative; for dim V > m it measures m-dimensional surfaces in V, such as the graph y ↦ (y, γ y) of a differentiable function, whose derivative is always injective.

Differentiability is required at the points of s, not merely within s, so that the Jacobian is the measurable function x ↦ (fderiv ℝ f x).normDet. For a Lipschitz map, Rademacher's theorem provides this at almost every point.

The argument

The linear case is Mathlib's LinearMap.euclideanHausdorffMeasure_image_eq_normDet_mul_volume: μHE[m] (A '' s) = J A · vol s. If f is approximated on s by an injective linear map A up to δ, in the sense of ApproximatesLinearOn, and ‖x‖ ≤ K ‖A x‖, then f ∘ A⁻¹ is (1 + δ K)-Lipschitz on A '' s and A ∘ f⁻¹ is (1 - δ K)⁻¹-Lipschitz on f '' s. Since a L-Lipschitz map increases μHE[m] by at most Lᵐ, the image measure μHE[m] (f '' s) lies between (1 - δ K)ᵐ J A vol s and (1 + δ K)ᵐ J A vol s (ApproximatesLinearOn.euclideanHausdorffMeasure_image_le, ApproximatesLinearOn.ofReal_normDet_mul_volume_le).

To globalize, fix τ > 1. The injective linear maps form an open set, on which J is continuous and positive (ContinuousLinearMap.continuous_normDet); cover it by countably many balls on each of which J varies by a factor at most τ and the antilipschitz constant is uniform. Splitting s according to which ball contains fderiv ℝ f x, and then by Mathlib's partition exists_partition_approximatesLinearOn_of_hasFDerivWithinAt, gives countably many disjoint measurable pieces on which both the integral and the image measure are within a factor τ³ of J A vol. The images of the pieces are disjoint and measurable (Lusin–Souslin), so summing gives the two inequalities up to τ³, and τ → 1 gives the formula.

Main declarations

• ApproximatesLinearOn.euclideanHausdorffMeasure_image_le, ApproximatesLinearOn.ofReal_normDet_mul_volume_le: the area formula up to a controlled factor for a map approximated by an injective linear map.
• MeasureTheory.lintegral_normDet_fderiv_eq_euclideanHausdorffMeasure_image: the area formula.
• MeasureTheory.euclideanHausdorffMeasure_image_le_lintegral_normDet: the resulting upper bound for the image of a map that factors through a 1-Lipschitz map.

References

• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, Section 3.3 (the area formula), whose proof for injective maps with positive Jacobian this follows.
• H. Federer, Geometric Measure Theory, 3.2.3.

theorem ApproximatesLinearOn.euclideanHausdorffMeasure_image_le {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {A : U →L[ℝ] V} {s : Set U} {δ K : NNReal} (hf : ApproximatesLinearOn f A s δ) (hA : AntilipschitzWith K ⇑A) : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)) (f '' s) ≤ ↑((1 + δ * K) ^ Module.finrank ℝ U) * (ENNReal.ofReal (↑A).normDet * MeasureTheory.volume s)

Upper area bound near a linear map. If f is approximated on s up to δ by a linear map A with ‖x‖ ≤ K ‖A x‖, then μHE[m] (f '' s) ≤ (1 + δ K)ᵐ J A vol s, where m = dim U and J A = A.normDet.

theorem ApproximatesLinearOn.ofReal_normDet_mul_volume_le {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {A : U →L[ℝ] V} {s : Set U} {δ K : NNReal} (hf : ApproximatesLinearOn f A s δ) (hA : AntilipschitzWith K ⇑A) (hδ : δ * K < 1) : ENNReal.ofReal (↑A).normDet * MeasureTheory.volume s ≤ ↑((1 - δ * K)⁻¹ ^ Module.finrank ℝ U) * (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)) (f '' s)

Lower area bound near a linear map. If f is approximated on s up to δ by a linear map A with ‖x‖ ≤ K ‖A x‖ and δ K < 1, then J A vol s ≤ (1 - δ K)⁻ᵐ μHE[m] (f '' s), where m = dim U and J A = A.normDet.

theorem MeasureTheory.lintegral_normDet_fderiv_eq_euclideanHausdorffMeasure_image {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {s : Set U} [FiniteDimensional ℝ V] (hs : MeasurableSet s) (hd : ∀ x ∈ s, DifferentiableAt ℝ f x) (hinj : ∀ x ∈ s, Function.Injective ⇑(fderiv ℝ f x)) (hf : Set.InjOn f s) : ∫⁻ (x : U) in s, ENNReal.ofReal (↑(fderiv ℝ f x)).normDet = (Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)) (f '' s)

The area formula for injective maps with injective derivative. Let U and V be finite-dimensional real inner product spaces and let f : U → V be injective on a measurable set s, differentiable at every point of s with injective derivative. Then the integral over s of the dim U-dimensional Jacobian (fderiv ℝ f x).normDet is the dim U-dimensional Euclidean Hausdorff measure of f '' s.

theorem MeasureTheory.euclideanHausdorffMeasure_image_le_lintegral_normDet {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {s : Set U} [FiniteDimensional ℝ V] {X : Type u_3} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {h : U → X} {g : U → V} {g' : U → U →L[ℝ] V} {p : V → X} (hs : MeasurableSet s) (hp : LipschitzOnWith 1 p (g '' s)) (hpg : ∀ x ∈ s, p (g x) = h x) (hg : ∀ x ∈ s, HasFDerivAt g (g' x) x) (hg' : ∀ x ∈ s, Function.Injective ⇑(g' x)) (hinj : Set.InjOn g s) : (Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)) (h '' s) ≤ ∫⁻ (x : U) in s, ENNReal.ofReal (↑(g' x)).normDet

Area bound through a 1-Lipschitz factorization. If h factors on a measurable set s as p ∘ g, where p is 1-Lipschitz on g '' s and g is injective on s with injective derivatives g' x, then μHE[m] (h '' s) ≤ ∫⁻ x in s, J (g' x), where m = dim U and J = normDet. The target of h is an arbitrary extended metric space.