The density theorem for rectifiable sets

Let E be a countably k-rectifiable subset of a finite-dimensional real inner product space, measurable for the normalized Euclidean Hausdorff measure μHE[k], with locally finite μHE[k] measure. The density theorem states that E has k-dimensional density one at μHE[k]-almost every point of E:

μHE[k] (E ∩ closedBall x r) / (ω_k r ^ k) → 1 as r → 0⁺,

where ω_k r ^ k is the volume of a ball of radius r in EuclideanSpace ℝ (Fin k) (TauCeti.CountablyRectifiable.ae_tendsto_euclideanHausdorffMeasure_inter_closedBall_div). Local finiteness cannot be dropped: in the plane, the union of the lines through pairs of points of a countable dense set is countably 1-rectifiable but has infinite μHE[1] measure in every ball.

The density theorem is the first step towards approximate tangent planes of rectifiable sets, and the form in which the structure theorem for sets of finite perimeter identifies the perimeter measure with Hausdorff measure on the reduced boundary.

Main results

• TauCeti.CountablyRectifiable.ae_tendsto_euclideanHausdorffMeasure_inter_closedBall_div: the density theorem.

The argument

Up to a null set, E is covered by images of Borel pieces on which a Lipschitz parametrization is within a relative error δ of an injective linear map A (LipschitzWith.exists_linear_approximation_cover). On each piece, the parametrization is (1 + δ)-Lipschitz with (1 - δ)⁻¹-Lipschitz inverse when read from the image of the piece under the approximating injective linear map A (TauCeti.lipschitzOnWith_and_antilipschitzWith_of_approx). This image lies in the k-plane range A, so the upper and lower densities of E on the piece lie between ((1 + δ) / (1 - δ)) ^ (±k) almost everywhere (Isometry.ae_limsup_le_and_le_liminf_euclideanHausdorffMeasure_inter_closedBall_div), since the part of E outside the piece has density zero at almost every point of the piece (TauCeti.ae_tendsto_euclideanHausdorffMeasure_inter_closedBall_div and TauCeti.limsup_measure_inter_div_le_of_tendsto_diff). Letting δ → 0 gives density one.

References

• L. Simon, Lectures on Geometric Measure Theory, §11 (the density of rectifiable sets).
• H. Federer, Geometric Measure Theory, 3.2.18 and 3.2.19 (decomposition of Lipschitz maps into pieces close to linear maps, and densities of rectifiable sets).
• P. Mattila, Geometry of Sets and Measures in Euclidean Spaces, Theorem 16.2.

theorem TauCeti.CountablyRectifiable.ae_tendsto_euclideanHausdorffMeasure_inter_closedBall_div {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {k : ℕ} {E : Set V} (hE : CountablyRectifiable k E) (hEm : MeasureTheory.NullMeasurableSet E (MeasureTheory.Measure.euclideanHausdorffMeasure k)) [MeasureTheory.IsLocallyFiniteMeasure ((MeasureTheory.Measure.euclideanHausdorffMeasure k).restrict E)] : ∀ᵐ (x : V) ∂MeasureTheory.Measure.euclideanHausdorffMeasure k, x ∈ E → Filter.Tendsto (fun (r : ℝ) => (MeasureTheory.Measure.euclideanHausdorffMeasure k) (E ∩ Metric.closedBall x r) / MeasureTheory.volume (Metric.closedBall 0 r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)

The density theorem for rectifiable sets. A countably k-rectifiable subset E of a finite-dimensional real inner product space, measurable for μHE[k] and with locally finite μHE[k] measure, has k-dimensional density one at μHE[k]-almost every point of E: μHE[k] (E ∩ closedBall x r) / (ω_k r ^ k) → 1 as r → 0⁺, where ω_k r ^ k is the volume of a ball of radius r in EuclideanSpace ℝ (Fin k).