Densities for the Euclidean Hausdorff measure under bi-Lipschitz maps and in k-planes

The k-dimensional density of a set S in a metric space at a point x compares μHE[k] (S ∩ closedBall x r) with ω_k r ^ k, the volume of a ball of radius r in EuclideanSpace ℝ (Fin k). This file proves general facts about these densities, none of which involves rectifiability:

• a map that is b-Lipschitz on G with a-Lipschitz inverse moves a point of density one of G to a point of ψ '' G whose upper and lower densities lie between (a b) ^ (-k) and (a b) ^ k;
• Lebesgue's density theorem in a k-plane: every subset of an isometric copy of EuclideanSpace ℝ (Fin k) has density one at almost every one of its points. This is transported from Mathlib's Besicovitch.ae_tendsto_measure_inter_div;
• combining the two, every subset of a bi-Lipschitz image of a subset of a k-plane has its densities between (a b) ^ (-k) and (a b) ^ k almost everywhere;
• removing a part of density zero from a set does not lower its upper density.

Together with the zero-density theorem TauCeti.ae_tendsto_euclideanHausdorffMeasure_inter_closedBall_div, these are the ingredients of the density theorem for rectifiable sets.

Main results

• LipschitzOnWith.limsup_euclideanHausdorffMeasure_image_inter_closedBall_div_le and LipschitzOnWith.le_liminf_euclideanHausdorffMeasure_image_inter_closedBall_div: densities under bi-Lipschitz maps.
• Isometry.ae_tendsto_euclideanHausdorffMeasure_inter_closedBall_div: Lebesgue's density theorem for subsets of an isometric copy of k-dimensional Euclidean space.
• Isometry.ae_limsup_le_and_le_liminf_euclideanHausdorffMeasure_inter_closedBall_div: density bounds almost everywhere on a bi-Lipschitz image of a subset of a k-plane.
• TauCeti.limsup_measure_inter_div_le_of_tendsto_diff: a part of a set with density zero does not contribute to the upper density.

References

• L. Simon, Lectures on Geometric Measure Theory, §11.
• P. Mattila, Geometry of Sets and Measures in Euclidean Spaces, Theorem 16.2.

theorem TauCeti.limsup_measure_inter_div_le_of_tendsto_diff {α : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {E S : Set X} {t : α → Set X} {d : α → ENNReal} {l : Filter α} (h : Filter.Tendsto (fun (r : α) => μ (E \ S ∩ t r) / d r) l (nhds 0)) : Filter.limsup (fun (r : α) => μ (E ∩ t r) / d r) l ≤ Filter.limsup (fun (r : α) => μ (E ∩ S ∩ t r) / d r) l

Discarding a part of E whose density quotients tend to zero does not lower the upper density: if μ (E \ S ∩ t r) / d r → 0, then the limsup of μ (E ∩ t r) / d r is at most that of μ (E ∩ S ∩ t r) / d r.

theorem LipschitzOnWith.limsup_euclideanHausdorffMeasure_image_inter_closedBall_div_le {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] {ψ : X → Y} {G : Set X} {a b : NNReal} {k : ℕ} {x : X} (hψ : LipschitzOnWith b ψ G) (hψ' : AntilipschitzWith a (G.domRestrict ψ)) (ha : 0 < a) (hx : x ∈ G) (hG : Filter.Tendsto (fun (r : ℝ) => (MeasureTheory.Measure.euclideanHausdorffMeasure k) (G ∩ Metric.closedBall x r) / MeasureTheory.volume (Metric.closedBall 0 r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)) : Filter.limsup (fun (r : ℝ) => (MeasureTheory.Measure.euclideanHausdorffMeasure k) (ψ '' G ∩ Metric.closedBall (ψ x) r) / MeasureTheory.volume (Metric.closedBall 0 r)) (nhdsWithin 0 (Set.Ioi 0)) ≤ ↑(a * b) ^ k

Upper density under a bi-Lipschitz map. Let ψ be b-Lipschitz on G with a-Lipschitz inverse. If G has k-dimensional density one at x ∈ G, then the upper k-dimensional density of ψ '' G at ψ x is at most (a b) ^ k.

theorem LipschitzOnWith.le_liminf_euclideanHausdorffMeasure_image_inter_closedBall_div {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] {ψ : X → Y} {G : Set X} {a b : NNReal} {k : ℕ} {x : X} (hψ : LipschitzOnWith b ψ G) (hψ' : AntilipschitzWith a (G.domRestrict ψ)) (ha : 0 < a) (hb : 0 < b) (hx : x ∈ G) (hG : Filter.Tendsto (fun (r : ℝ) => (MeasureTheory.Measure.euclideanHausdorffMeasure k) (G ∩ Metric.closedBall x r) / MeasureTheory.volume (Metric.closedBall 0 r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)) : (↑(a * b) ^ k)⁻¹ ≤ Filter.liminf (fun (r : ℝ) => (MeasureTheory.Measure.euclideanHausdorffMeasure k) (ψ '' G ∩ Metric.closedBall (ψ x) r) / MeasureTheory.volume (Metric.closedBall 0 r)) (nhdsWithin 0 (Set.Ioi 0))

Lower density under a bi-Lipschitz map. Let ψ be b-Lipschitz on G with a-Lipschitz inverse. If G has k-dimensional density one at x ∈ G, then the lower k-dimensional density of ψ '' G at ψ x is at least (a b) ^ (-k).

theorem Isometry.ae_tendsto_euclideanHausdorffMeasure_inter_closedBall_div {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {k : ℕ} {ι : EuclideanSpace ℝ (Fin k) → X} (hι : Isometry ι) {S : Set X} (hS : S ⊆ Set.range ι) : ∀ᵐ (x : X) ∂MeasureTheory.Measure.euclideanHausdorffMeasure k, x ∈ S → Filter.Tendsto (fun (r : ℝ) => (MeasureTheory.Measure.euclideanHausdorffMeasure k) (S ∩ Metric.closedBall x r) / MeasureTheory.volume (Metric.closedBall 0 r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)

Lebesgue's density theorem in a k-plane. Let ι be an isometry from k-dimensional Euclidean space into X. Every subset S of its range has k-dimensional density one at μHE[k]-almost every point of S. No measurability of S is needed.

theorem Isometry.ae_limsup_le_and_le_liminf_euclideanHausdorffMeasure_inter_closedBall_div {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {k : ℕ} {Y : Type u_2} [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] {ι : EuclideanSpace ℝ (Fin k) → X} (hι : Isometry ι) {G : Set X} (hGι : G ⊆ Set.range ι) {ψ : X → Y} {a b : NNReal} (hψ : LipschitzOnWith b ψ G) (hψ' : AntilipschitzWith a (G.domRestrict ψ)) (ha : 0 < a) (hb : 0 < b) {T : Set Y} (hT : T ⊆ ψ '' G) : ∀ᵐ (y : Y) ∂MeasureTheory.Measure.euclideanHausdorffMeasure k, y ∈ T → Filter.limsup (fun (r : ℝ) => (MeasureTheory.Measure.euclideanHausdorffMeasure k) (T ∩ Metric.closedBall y r) / MeasureTheory.volume (Metric.closedBall 0 r)) (nhdsWithin 0 (Set.Ioi 0)) ≤ ↑(a * b) ^ k ∧ (↑(a * b) ^ k)⁻¹ ≤ Filter.liminf (fun (r : ℝ) => (MeasureTheory.Measure.euclideanHausdorffMeasure k) (T ∩ Metric.closedBall y r) / MeasureTheory.volume (Metric.closedBall 0 r)) (nhdsWithin 0 (Set.Ioi 0))

Densities of a bi-Lipschitz image of a subset of a k-plane. Let ι be an isometry from k-dimensional Euclidean space into X, and let ψ be b-Lipschitz on a subset G of its range with a-Lipschitz inverse. Then every subset T of ψ '' G has upper density at most (a b) ^ k and lower density at least (a b) ^ (-k) at μHE[k]-almost every point of T.