Lipschitz images of Haar-null sets

A map from a finite-dimensional real normed space to one of at least the same dimension that is Lipschitz on a set s sends s to a null set whenever s is null, for any additive Haar measures on the source and the target. In dimension d the Hausdorff measure μH[d] is an additive Haar measure, so every additive Haar measure is mutually absolutely continuous with it. Lipschitz maps increase the Hausdorff d-measure by at most the factor K ^ d (LipschitzOnWith.hausdorffMeasure_image_le), and a set of zero Hausdorff d-measure has zero Hausdorff d'-measure for every d' ≥ d. The same factor K ^ d bounds the growth of the normalized Euclidean Hausdorff measure μHE[d], a constant multiple of μH[d].

Main statements

• LipschitzOnWith.addHaar_image_eq_zero — a map Lipschitz on a Haar-null set has a Haar-null image, from a finite-dimensional real normed space to one of at least the same dimension.
• LipschitzOnWith.euclideanHausdorffMeasure_image_le — a K-Lipschitz map increases μHE[d] by at most the factor K ^ d.

theorem LipschitzOnWith.addHaar_image_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (ν : MeasureTheory.Measure F) [ν.IsAddHaarMeasure] (hdim : Module.finrank ℝ E ≤ Module.finrank ℝ F) {K : NNReal} {f : E → F} {s : Set E} (hf : LipschitzOnWith K f s) (hs : μ s = 0) : ν (f '' s) = 0

Lipschitz maps preserve Haar-null sets. If f : E → F is Lipschitz on a set s that is null for an additive Haar measure μ on E, and E and F are finite-dimensional real normed spaces with finrank ℝ E ≤ finrank ℝ F, then f '' s is null for every additive Haar measure ν on F.

theorem LipschitzOnWith.euclideanHausdorffMeasure_image_le {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] [EMetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] {K : NNReal} {f : X → Y} {s : Set X} (hf : LipschitzOnWith K f s) (d : ℕ) : (MeasureTheory.Measure.euclideanHausdorffMeasure d) (f '' s) ≤ ↑K ^ d * (MeasureTheory.Measure.euclideanHausdorffMeasure d) s

A map that is K-Lipschitz on s increases the d-dimensional Euclidean Hausdorff measure of s by at most the factor K ^ d.