Countably rectifiable sets

A countably k-rectifiable set is covered, up to a null set for normalized Euclidean Hausdorff measure μHE[k], by countably many Lipschitz images of subsets of EuclideanSpace ℝ (Fin k). The domains need not be measurable, and neither measurability nor local finiteness of Hausdorff measure is part of rectifiability.

We prove closure under subsets, countable unions and null modifications, and transport by maps Lipschitz on the set. These operations allow rectifiable sets to be localized and their parametrizations to be composed without imposing regularity on the exceptional set. Patches are maps from subtypes, so even an empty target requires no arbitrary base point. In a finite-dimensional real normed space, the patches extend to Lipschitz maps defined on all of EuclideanSpace ℝ (Fin k) (TauCeti.CountablyRectifiable.exists_lipschitzWith_cover).

The image estimates use LipschitzOnWith.euclideanHausdorffMeasure_image_le, which explicitly compares the normalized measure with Mathlib's raw Hausdorff measure.

References

• L. Simon, Lectures on Geometric Measure Theory, §11 (countably rectifiable sets).

def TauCeti.CountablyRectifiable {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (k : ℕ) (s : Set X) : Prop

A set is countably k-rectifiable if countably many Lipschitz patches cover it up to μHE[k]-measure zero. No measurability or measure finiteness is required.

theorem TauCeti.countablyRectifiable_iff {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {k : ℕ} {s : Set X} : CountablyRectifiable k s ↔ ∃ (A : ℕ → Set (EuclideanSpace ℝ (Fin k))) (f : (i : ℕ) → ↑(A i) → X), (∀ (i : ℕ), ∃ (K : NNReal), LipschitzWith K (f i)) ∧ (MeasureTheory.Measure.euclideanHausdorffMeasure k) (s \ ⋃ (i : ℕ), Set.range (f i)) = 0

The Lipschitz-patch characterization of countable rectifiability.

theorem TauCeti.CountablyRectifiable.of_null {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {k : ℕ} {s : Set X} (hs : (MeasureTheory.Measure.euclideanHausdorffMeasure k) s = 0) : CountablyRectifiable k s

Every μHE[k]-null set is countably k-rectifiable.

@[simp]

theorem TauCeti.CountablyRectifiable.empty {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {k : ℕ} : CountablyRectifiable k ∅

theorem TauCeti.CountablyRectifiable.mono_ae {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {k : ℕ} {s t : Set X} (hs : CountablyRectifiable k s) (ht : t ≤ᵐ[MeasureTheory.Measure.euclideanHausdorffMeasure k] s) : CountablyRectifiable k t

An almost everywhere subset of a rectifiable set is rectifiable.

theorem TauCeti.CountablyRectifiable.mono {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {k : ℕ} {s t : Set X} (hs : CountablyRectifiable k s) (ht : t ⊆ s) : CountablyRectifiable k t

Arbitrary subsets of rectifiable sets are rectifiable; in particular this allows restriction to measurable sets without an additional measurability assumption.

theorem TauCeti.CountablyRectifiable.congr {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {k : ℕ} {s t : Set X} (hs : CountablyRectifiable k s) (hst : s =ᵐ[MeasureTheory.Measure.euclideanHausdorffMeasure k] t) : CountablyRectifiable k t

Countable rectifiability is independent of the representative modulo μHE[k].

theorem TauCeti.CountablyRectifiable.of_lipschitzWith {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {k : ℕ} {A : Set (EuclideanSpace ℝ (Fin k))} {f : ↑A → X} {K : NNReal} (hf : LipschitzWith K f) : CountablyRectifiable k (Set.range f)

A single Lipschitz patch is countably rectifiable.

theorem TauCeti.CountablyRectifiable.of_lipschitzOnWith {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {k : ℕ} {A : Set (EuclideanSpace ℝ (Fin k))} {f : EuclideanSpace ℝ (Fin k) → X} {K : NNReal} (hf : LipschitzOnWith K f A) : CountablyRectifiable k (f '' A)

A Lipschitz image of a subset of k-dimensional Euclidean space is countably k-rectifiable.

theorem TauCeti.CountablyRectifiable.euclidean {k : ℕ} (A : Set (EuclideanSpace ℝ (Fin k))) : CountablyRectifiable k A

Every subset of k-dimensional Euclidean space is countably k-rectifiable.

theorem TauCeti.CountablyRectifiable.sUnion {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {k : ℕ} {S : Set (Set X)} (hS : S.Countable) (hs : ∀ s ∈ S, CountablyRectifiable k s) : CountablyRectifiable k (⋃₀ S)

A countable collection of rectifiable sets has rectifiable union.

theorem TauCeti.CountablyRectifiable.iUnion {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {k : ℕ} {ι : Type u_3} [Countable ι] {s : ι → Set X} (hs : ∀ (i : ι), CountablyRectifiable k (s i)) : CountablyRectifiable k (⋃ (i : ι), s i)

Unions indexed by any countable type preserve rectifiability, including an empty index.

theorem TauCeti.CountablyRectifiable.union {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {k : ℕ} {s t : Set X} (hs : CountablyRectifiable k s) (ht : CountablyRectifiable k t) : CountablyRectifiable k (s ∪ t)

Binary unions of rectifiable sets are rectifiable.

theorem TauCeti.CountablyRectifiable.image {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] [EMetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] {k : ℕ} {s : Set X} (hs : CountablyRectifiable k s) {g : X → Y} {K : NNReal} (hg : LipschitzOnWith K g s) : CountablyRectifiable k (g '' s)

A map Lipschitz on a rectifiable set has rectifiable image. No measurability of the set or its patch domains is needed.

theorem TauCeti.CountablyRectifiable.isometry_image_iff {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] [EMetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] {k : ℕ} {s : Set X} {f : X → Y} (hf : Isometry f) : CountablyRectifiable k (f '' s) ↔ CountablyRectifiable k s

Isometric embeddings preserve and reflect countable rectifiability, without requiring surjectivity or a nonempty source.

@[simp]

theorem TauCeti.CountablyRectifiable.isometryEquiv_image_iff {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] [EMetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] {k : ℕ} {s : Set X} {e : X ≃ᵢ Y} : CountablyRectifiable k (⇑e '' s) ↔ CountablyRectifiable k s

Isometric equivalences preserve countable rectifiability in both directions.

theorem TauCeti.countablyRectifiable_congr {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {k : ℕ} {s t : Set X} (hst : s =ᵐ[MeasureTheory.Measure.euclideanHausdorffMeasure k] t) : CountablyRectifiable k s ↔ CountablyRectifiable k t

Countable rectifiability is invariant under equality almost everywhere for normalized Hausdorff measure, without a measurability assumption on either representative.

theorem TauCeti.CountablyRectifiable.exists_lipschitzWith_cover {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {k : ℕ} {s : Set V} (hs : CountablyRectifiable k s) : ∃ (F : ℕ → EuclideanSpace ℝ (Fin k) → V), (∀ (n : ℕ), ∃ (K : NNReal), LipschitzWith K (F n)) ∧ (MeasureTheory.Measure.euclideanHausdorffMeasure k) (s \ ⋃ (n : ℕ), Set.range (F n)) = 0

A countably k-rectifiable subset of a finite-dimensional real normed space is covered, up to a μHE[k]-null set, by the ranges of countably many Lipschitz maps defined on all of EuclideanSpace ℝ (Fin k).