Finite-length continua

Compact connected subsets of the Euclidean plane with finite Hausdorff one-measure have a Lipschitz parametrization. This is the Eilenberg--Harrold finite-length continuum theorem.

theorem LeanPool.Besicovitch.hausdorffMeasure_one_inter_closedBall_ge {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {s : Set X} (hs : IsPreconnected s) {x y : X} (hx : x ∈ s) (hy : y ∈ s) {r : ℝ} (hry : r ≤ dist x y) : ENNReal.ofReal r ≤ (MeasureTheory.Measure.hausdorffMeasure 1) (s ∩ Metric.closedBall x r)

A connected set reaching distance r from x has at least r units of length inside the closed r-ball about x.

theorem LeanPool.Besicovitch.IsConnected.exists_lipschitzWith_range_eq {s : Set (EuclideanSpace ℝ (Fin 2))} (hs : IsConnected s) (hsc : IsCompact s) (hmeasure : (MeasureTheory.Measure.hausdorffMeasure 1) s ≠ ⊤) : ∃ (K : NNReal) (f : ℝ → EuclideanSpace ℝ (Fin 2)), LipschitzWith K f ∧ Set.range f = s

Eilenberg--Harrold. A compact connected planar set of finite length is the range of a global Lipschitz curve.

theorem LeanPool.Besicovitch.IsConnected.isCountablyOneRectifiable_of_isCompact {s : Set (EuclideanSpace ℝ (Fin 2))} (hs : IsConnected s) (hsc : IsCompact s) (hmeasure : (MeasureTheory.Measure.hausdorffMeasure 1) s ≠ ⊤) : IsCountablyOneRectifiable s

A compact connected planar set of finite Hausdorff one-measure is countably one-rectifiable.