Zero Jacobians and the area formula for injective Lipschitz maps

Let U and V be finite-dimensional real inner product spaces, m = dim U, and let J f x = (fderiv ℝ f x).normDet be the m-dimensional Jacobian of f : U → V. This file shows that the points where f is not differentiable with injective derivative do not matter for the area formula of a Lipschitz map:

• Zero Jacobians have null images. If f is differentiable at every point of a set s and J f = 0 on s, then μHE[m] (f '' s) = 0. No Lipschitz, measurability, or injectivity hypothesis is needed. This is the rectangular counterpart of Mathlib's addHaar_image_eq_zero_of_det_fderivWithin_eq_zero, measured by the normalized Hausdorff measure μHE[m] of the target rather than by its volume.
• The area formula for injective Lipschitz maps. If f is Lipschitz and injective on a measurable set s, then ∫⁻ x in s, J f x = μHE[m] (f '' s), with a weighted form for an arbitrary nonnegative weight on the target. Unlike MeasureTheory.lintegral_normDet_fderiv_eq_euclideanHausdorffMeasure_image, neither differentiability nor injectivity of the derivative is assumed.

The argument

For the first statement, f is lifted to g ε x = (f x, ε x) in the Euclidean product of V and U. For ε ≠ 0 the lift is injective with injective derivative, so the injective area formula applies to it, and f is the composition of g ε with the 1-Lipschitz first projection. Hence μHE[m] (f '' s) ≤ ∫⁻ x in s, J (g ε) x. As ε → 0, the derivative of g ε tends to the derivative of x ↦ (f x, 0), whose Jacobian is J f x = 0. On bounded pieces of s where fderiv ℝ f is bounded, dominated convergence shows that the integrals tend to zero.

For the second statement, Rademacher's theorem LipschitzWith.ae_differentiableAt makes the set of nondifferentiability points null, so its image is null, while the first statement makes the image of the points with zero Jacobian null. On the remaining points the derivative is injective and the regular injective area formula applies.

Main declarations

• TauCeti.euclideanHausdorffMeasure_image_eq_zero_of_normDet_fderiv_eq_zero: zero Jacobians have null images.
• LipschitzWith.euclideanHausdorffMeasure_image_setOf_normDet_fderiv_eq_zero: the image of the set where the Jacobian of a Lipschitz map vanishes is null.
• LipschitzWith.exists_linear_approximation_cover: for every δ > 0, countably many disjoint Borel patches on which the map is within relative error δ of an injective linear map cover the image up to a null set, using TauCeti.exists_partition_linear_approximation_of_hasFDerivWithinAt on the regular points.
• LipschitzWith.exists_bilipschitz_cover: countably many disjoint Borel patches with Lipschitz inverse coordinates cover the image up to a null set; these are the patches of the previous result for relative error 1 / 2.
• LipschitzWith.lintegral_image_eq_lintegral_normDet_fderiv_mul: the weighted area formula for a Lipschitz map injective on a measurable set.
• LipschitzWith.lintegral_normDet_fderiv_eq_euclideanHausdorffMeasure_image: the area formula for a Lipschitz map injective on a measurable set.

References

• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, Section 3.3 (the area formula), whose proof of the zero Jacobian statement for Lipschitz maps, by lifting to x ↦ (f x, ε x), this file follows.
• H. Federer, Geometric Measure Theory, 3.2.18 (pieces on which a Lipschitz map is close to an injective linear map).

theorem TauCeti.measurableSet_setOf_differentiableAt_normDet_ne_zero {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U] [BorelSpace U] (f : U → V) : MeasurableSet {x : U | DifferentiableAt ℝ f x ∧ (↑(fderiv ℝ f x)).normDet ≠ 0}

The set of differentiability points with nonzero geometric Jacobian is Borel measurable.

theorem TauCeti.euclideanHausdorffMeasure_image_eq_zero_of_normDet_fderiv_eq_zero {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {s : Set U} (hd : ∀ x ∈ s, DifferentiableAt ℝ f x) (h0 : ∀ x ∈ s, (↑(fderiv ℝ f x)).normDet = 0) : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)) (f '' s) = 0

Zero Jacobians have null images. Let U and V be finite-dimensional real inner product spaces. If f : U → V is differentiable at every point of s and its dim U-dimensional Jacobian (fderiv ℝ f x).normDet vanishes there, then f '' s is null for the dim U-dimensional Euclidean Hausdorff measure. The set s need not be measurable.

theorem LipschitzWith.euclideanHausdorffMeasure_image_compl_setOf_regular {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {K : NNReal} (hf : LipschitzWith K f) : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)) (f '' {x : U | DifferentiableAt ℝ f x ∧ (↑(fderiv ℝ f x)).normDet ≠ 0}ᶜ) = 0

A Lipschitz map sends the complement of its regular points, where it is differentiable with nonzero Jacobian, to a null set.

theorem LipschitzWith.exists_linear_approximation_cover {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {K : NNReal} (hf : LipschitzWith K f) {δ : ℝ} (hδ : 0 < δ) : ∃ (P : ℕ → Set U) (A : ℕ → U →L[ℝ] V), (∀ (n : ℕ), MeasurableSet (P n)) ∧ Pairwise (Function.onFun Disjoint P) ∧ (∀ (n : ℕ), (P n).Nonempty → Function.Injective ⇑(A n)) ∧ (∀ (n : ℕ), ∀ x ∈ P n, ∀ y ∈ P n, ‖f x - f y - (A n) (x - y)‖ ≤ δ * ‖(A n) (x - y)‖) ∧ (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)) (Set.range f \ ⋃ (n : ℕ), f '' P n) = 0

Linear approximation of a Lipschitz map on pieces. For every δ > 0, the image of a Lipschitz map f : U → V is covered, up to a μHE[dim U]-null set, by the images of countably many disjoint Borel pieces P n, each with an approximating linear map A n that is injective whenever the piece is nonempty and satisfies ‖f x - f y - A n (x - y)‖ ≤ δ ‖A n (x - y)‖ on the piece.

theorem LipschitzWith.exists_bilipschitz_cover {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {K : NNReal} (hf : LipschitzWith K f) : ∃ (A : ℕ → Set U), (∀ (n : ℕ), MeasurableSet (A n)) ∧ Pairwise (Function.onFun Disjoint A) ∧ (∀ (n : ℕ), ∃ (L : NNReal), AntilipschitzWith L ((A n).domRestrict f)) ∧ (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)) (Set.range f \ ⋃ (n : ℕ), f '' A n) = 0

The image of a Lipschitz map is covered up to a null set by images of countably many disjoint Borel sets on which the map has a Lipschitz inverse. The forward Lipschitz bound is inherited from the original map.

theorem LipschitzWith.euclideanHausdorffMeasure_image_setOf_normDet_fderiv_eq_zero {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {K : NNReal} (hf : LipschitzWith K f) : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)) (f '' {x : U | (↑(fderiv ℝ f x)).normDet = 0}) = 0

Sard's lemma for Lipschitz maps. The image of the set where the dim U-dimensional Jacobian of a Lipschitz map f : U → V vanishes is null for the dim U-dimensional Euclidean Hausdorff measure.

theorem LipschitzWith.lintegral_image_eq_lintegral_normDet_fderiv_mul {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {s : Set U} {K : NNReal} (hf : LipschitzWith K f) (hs : MeasurableSet s) (hinj : Set.InjOn f s) (g : V → ENNReal) : ∫⁻ (y : V) in f '' s, g y ∂MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U) = ∫⁻ (x : U) in s, ENNReal.ofReal (↑(fderiv ℝ f x)).normDet * g (f x)

The weighted area formula for injective Lipschitz maps. If f : U → V is Lipschitz and injective on a measurable set s, then for every weight g : V → ℝ≥0∞ the integral of g over f '' s for the dim U-dimensional Euclidean Hausdorff measure is the integral over s of g ∘ f weighted by the Jacobian (fderiv ℝ f x).normDet. The weight need not be measurable.

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

The area formula for injective Lipschitz maps. If f : U → V is Lipschitz and injective on a measurable set s, 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.