Arclength parametrization of simple closed curves

A continuous rectifiable curve with equal endpoint values and no repetitions on the half-open parameter interval has an arclength parametrization with exactly the same simplicity property. The parametrization is 1-Lipschitz, has unit variation speed, and traces the original image. The repetition characterization includes the zero-length case: its length interval is a singleton. Values outside the length interval are unspecified.

Together with the increasing arclength homeomorphism, this permits transporting geometric constructions on simple closed curves to a Lipschitz parameter without losing their orientation or introducing repeated points.

The construction uses Mathlib's naturalParameterization and its unit-speed theorem, together with HasConstantSpeedOnWith.lipschitzOnWith; there is no additional curve or length carrier.

References

• L. Ambrosio, N. Gigli, G. Savaré, Gradient Flows, second edition, §1.1 (arclength parametrization of metric curves).

theorem BoundedVariationOn.injOn_naturalParameterization_Ico {X : Type u_1} [MetricSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : BoundedVariationOn γ (Set.Icc a b)) (hcont : ContinuousOn γ (Set.Icc a b)) (hinj : Set.InjOn γ (Set.Ico a b)) (hab : a ≤ b) : Set.InjOn (naturalParameterization γ (Set.Icc a b) a) (Set.Ico 0 (eVariationOn γ (Set.Icc a b)).toReal)

Half-open injectivity of a continuous rectifiable curve passes to its natural parameterization on [0, L).

theorem BoundedVariationOn.exists_simple_closed_arclength_parametrization {X : Type u_1} [MetricSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : BoundedVariationOn γ (Set.Icc a b)) (hcont : ContinuousOn γ (Set.Icc a b)) (hinj : Set.InjOn γ (Set.Ico a b)) (hclosed : γ a = γ b) (hab : a ≤ b) : ∃ (g : ℝ → X), LipschitzOnWith 1 g (Set.Icc 0 (eVariationOn γ (Set.Icc a b)).toReal) ∧ HasUnitSpeedOn g (Set.Icc 0 (eVariationOn γ (Set.Icc a b)).toReal) ∧ Set.EqOn (g ∘ variationOnFromTo γ (Set.Icc a b) a) γ (Set.Icc a b) ∧ g 0 = γ a ∧ g (eVariationOn γ (Set.Icc a b)).toReal = γ b ∧ g '' Set.Icc 0 (eVariationOn γ (Set.Icc a b)).toReal = γ '' Set.Icc a b ∧ ∀ u ∈ Set.Icc 0 (eVariationOn γ (Set.Icc a b)).toReal, ∀ v ∈ Set.Icc 0 (eVariationOn γ (Set.Icc a b)).toReal, g u = g v ↔ u = v ∨ u = 0 ∧ v = (eVariationOn γ (Set.Icc a b)).toReal ∨ u = (eVariationOn γ (Set.Icc a b)).toReal ∧ v = 0

A rectifiable simple closed curve admits a unit-speed Lipschitz arclength parametrization. The endpoints are preserved, the trace is unchanged, and equality of two values occurs exactly at equal parameters or at the two endpoints. The statement also holds on a singleton interval.