Rectifiable and purely unrectifiable parts

A finite measurable set splits into a countably one-rectifiable part and a measurable purely one-unrectifiable remainder. The proof maximizes the measure captured by countably many Lipschitz curves; it does not assume a decomposition theorem from outside Mathlib.

theorem LeanPool.Besicovitch.measurableSet_iUnion_range_of_lipschitz {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {f : ℕ → ℝ → X} (hf : ∀ (i : ℕ), ∃ (K : NNReal), LipschitzWith K (f i)) : MeasurableSet (⋃ (i : ℕ), Set.range (f i))

A countable union of ranges of Lipschitz curves is measurable.

theorem LeanPool.Besicovitch.IsCountablyOneRectifiable.exists_measurable_cover {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {s : Set X} (hs : IsCountablyOneRectifiable s) : ∃ (t : Set X), MeasurableSet t ∧ IsCountablyOneRectifiable t ∧ (MeasureTheory.Measure.hausdorffMeasure 1) (s \ t) = 0

A rectifiable set is covered up to a null set by a measurable rectifiable set.

theorem LeanPool.Besicovitch.exists_rectifiable_pure_decomposition {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [Nonempty X] {s : Set X} (hs : MeasurableSet s) (hfinite : (MeasureTheory.Measure.hausdorffMeasure 1) s < ⊤) : ∃ (r : Set X) (p : Set X), MeasurableSet r ∧ MeasurableSet p ∧ r ⊆ s ∧ p = s \ r ∧ IsCountablyOneRectifiable r ∧ IsPurelyOneUnrectifiable p

Every finite measurable set is the disjoint union of a rectifiable part and a purely unrectifiable part.