Hausdorff measure, Lipschitz maps, and null sets

When a subset of ℝ³ has vanishing one-dimensional Hausdorff measure, its Lipschitz image has vanishing Lebesgue measure (volume_image_eq_zero_of_hausdorffMeasure_one_eq_zero), and consequently almost every radius r avoids the image (ae_notMem_image_of_hausdorffMeasure_one_eq_zero). The classical fact that a null set cannot contain a whole sphere for almost every radius, used in the proof of lem:aniso:annulus, is ae_forall_norm_ne_of_hausdorffMeasure_one_eq_zero: for a null set S, almost every r has ∂B(r) ∩ S = ∅.

Lipschitz bounds for the Hausdorff measure

theorem CIV.hausdorffMeasure_image_le_of_lipschitzWith {f : CKN.Foundation.Parabolic.Vec3 → ℝ} {K : NNReal} (hf : LipschitzWith K f) (S : Set CKN.Foundation.Parabolic.Vec3) : (MeasureTheory.Measure.hausdorffMeasure 1) (f '' S) ≤ ↑K * (MeasureTheory.Measure.hausdorffMeasure 1) S

A Lipschitz map f : Vec3 → ℝ cannot increase the one-dimensional Hausdorff measure by more than the Lipschitz constant: μH¹(f '' S) ≤ K · μH¹(S).

theorem CIV.volume_image_eq_zero_of_hausdorffMeasure_one_eq_zero {f : CKN.Foundation.Parabolic.Vec3 → ℝ} {K : NNReal} (hf : LipschitzWith K f) {S : Set CKN.Foundation.Parabolic.Vec3} (hS : (MeasureTheory.Measure.hausdorffMeasure 1) S = 0) : MeasureTheory.volume (f '' S) = 0

If S has vanishing one-dimensional Hausdorff measure, its Lipschitz image has vanishing Lebesgue measure in ℝ.

theorem CIV.ae_notMem_image_of_hausdorffMeasure_one_eq_zero {f : CKN.Foundation.Parabolic.Vec3 → ℝ} {K : NNReal} (hf : LipschitzWith K f) {S : Set CKN.Foundation.Parabolic.Vec3} (hS : (MeasureTheory.Measure.hausdorffMeasure 1) S = 0) : ∀ᵐ (r : ℝ), r ∉ f '' S

If S has vanishing one-dimensional Hausdorff measure, almost every real number r lies outside the Lipschitz image f '' S.

Spheres avoiding a null set

theorem CIV.ae_forall_norm_ne_of_hausdorffMeasure_one_eq_zero {S : Set CKN.Foundation.Parabolic.Vec3} (hS : (MeasureTheory.Measure.hausdorffMeasure 1) S = 0) : ∀ᵐ (r : ℝ), ∀ x ∈ S, ‖x‖ ≠ r

For a subset S of ℝ³ with vanishing one-dimensional Hausdorff measure, almost every radius r has the property that no point of S lies on the sphere ‖x‖ = r. This is the classical fact behind the choice of a radius R with ∂B(R) disjoint from the singular set S₀ in the proof of lem:aniso:annulus.