Arc-length reparametrization of regular Riemannian curves

Every regular C¹ curve on a compact interval admits a unit-speed forward reparametrization, whether it is C¹ on an open parameter set containing the interval or only within the interval itself. The new parameter is the accumulated Riemannian speed

s(t) = ∫ r in a..t, ‖γ'(r)‖.

Extending the speed by constants outside [a, b] makes s a C¹ increasing bijection of ℝ with positive derivative. Its inverse ψ is C¹, with derivative the reciprocal speed, and the chain rule then gives ‖(γ ∘ ψ)'‖ = 1. Besides unit speed, the theorems record the inverse identities, endpoint values, monotonicity, and invariance of Manifold.pathELength, making the results usable without unfolding their construction.

The first part of the file computes lengths from speeds: the length of a C¹ curve is the integral of its speed, a curve of constant speed C on (a, b) has length C * (b - a), and the length L and energy E over [a, b] satisfy the Cauchy–Schwarz bound L ^ 2 ≤ 2 * (b - a) * E, so that energy less than (b - a) / 2 forces length less than b - a.

Main results

• ContMDiffOn.continuousOn_norm_curveVelocityWithin: the speed of a C¹ curve is continuous on a parameter set with unique derivatives.
• ContMDiffOn.pathELength_eq_ofReal_integral_norm_curveVelocityWithin: the Riemannian length of a C¹ curve over a compact interval is the integral of its speed.
• TauCeti.Manifold.pathELength_eq_of_norm_curveVelocity_eq: a curve of constant speed C on (a, b) has length C * (b - a).
• TauCeti.Manifold.pathELength_le_ofReal_sqrt_energy_of_intervalIntegrable: the length L and the energy E of a curve with square-integrable speed over [a, b] satisfy L ^ 2 ≤ 2 * (b - a) * E; ContMDiffOn.pathELength_le_ofReal_sqrt_energy is the C¹ case.
• TauCeti.Manifold.pathELength_lt_of_energy_lt_of_intervalIntegrable and ContMDiffOn.pathELength_lt_of_energy_lt: energy less than (b - a) / 2 forces length less than b - a.
• TauCeti.Manifold.exists_unit_speed_reparametrization: a regular curve, C¹ on an open set containing [a, b], has a C¹, unit-speed reparametrization on the interval from zero to its length.
• TauCeti.Manifold.exists_unit_speed_reparametrization_Icc: the same for a curve which is only C¹ within [a, b], with velocities read within the parameter intervals.

References

• J. M. Lee, Introduction to Riemannian Manifolds, second edition, Proposition 2.49(a).
• J. Milnor, Morse Theory, Annals of Mathematics Studies 51, Princeton, 1963, §12, for the comparison of length and energy.
• The proof is adapted from LeeLib/Ch02/ArcLengthReparametrization.lean in the Apache-2.0 frenzymath/Poincare-Conjecture repository, revision 24f32e4d600878bfaac6bc2f2f9324175571c321. This version works at the C¹ regularity of the theorem and uses Mathlib's Riemannian bundle and path-length APIs.

Length as the integral of speed

theorem ContMDiffOn.continuousOn_norm_curveVelocityWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ s) (hs : UniqueMDiff[s]) : ContinuousOn (fun (t : ℝ) => ‖TauCeti.Manifold.curveVelocityWithin I γ s t‖) s

The Riemannian speed of a C¹ curve, read within a parameter set with unique derivatives, is continuous on that set.

theorem ContMDiffOn.pathELength_eq_ofReal_integral_norm_curveVelocityWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ s) (hs : UniqueMDiff[s]) {a b : ℝ} (hab : a ≤ b) (hsub : Set.Icc a b ⊆ s) : Manifold.pathELength I γ a b = ENNReal.ofReal (∫ (t : ℝ) in a..b, ‖TauCeti.Manifold.curveVelocityWithin I γ s t‖)

The Riemannian length of a C¹ curve over a compact interval inside its parameter set is the integral of its speed.

theorem ContMDiffOn.intervalIntegrable_norm_curveVelocity_sq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ s) (hs : UniqueMDiff[s]) {a b : ℝ} (hsub : Set.uIcc a b ⊆ s) : IntervalIntegrable (fun (t : ℝ) => ‖TauCeti.Manifold.curveVelocity I γ t‖ ^ 2) MeasureTheory.volume a b

The squared Riemannian speed of a C¹ curve is interval integrable between any two parameters of a parameter set with unique derivatives containing the interval between them.

theorem TauCeti.Manifold.pathELength_eq_of_norm_curveVelocity_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {γ : ℝ → M} {a b C : ℝ} (h : ∀ t ∈ Set.Ioo a b, ‖curveVelocity I γ t‖ = C) : Manifold.pathELength I γ a b = ENNReal.ofReal C * ENNReal.ofReal (b - a)

A curve whose Riemannian speed is C on the open interval (a, b) has length C * (b - a) from a to b. No regularity of the curve is assumed, and its velocities at a and b play no role.

theorem TauCeti.Manifold.pathELength_eq_of_norm_curveVelocity_eq_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {γ : ℝ → M} {a b : ℝ} (h : ∀ t ∈ Set.Ioo a b, ‖curveVelocity I γ t‖ = 1) : Manifold.pathELength I γ a b = ENNReal.ofReal (b - a)

A curve with unit Riemannian speed on the open interval (a, b) has length b - a from a to b.

Length and energy

theorem TauCeti.Manifold.pathELength_le_ofReal_sqrt_energy_of_intervalIntegrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {γ : ℝ → M} {a b : ℝ} (hab : a ≤ b) (hγ : IntervalIntegrable (fun (t : ℝ) => ‖curveVelocity I γ t‖ ^ 2) MeasureTheory.volume a b) : Manifold.pathELength I γ a b ≤ ENNReal.ofReal √(2 * (b - a) * energy I γ a b)

Length is controlled by energy. If the squared Riemannian speed of a curve is integrable on [a, b], its length L and its energy E over [a, b] satisfy L ^ 2 ≤ 2 * (b - a) * E. This is the Cauchy–Schwarz inequality for the speed ‖γ'‖ on [a, b]. No regularity of the curve is assumed, so this applies to curves with finitely many corners.

theorem TauCeti.Manifold.pathELength_lt_of_energy_lt_of_intervalIntegrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {γ : ℝ → M} {a b : ℝ} (hab : a < b) (hγ : IntervalIntegrable (fun (t : ℝ) => ‖curveVelocity I γ t‖ ^ 2) MeasureTheory.volume a b) (hE : energy I γ a b < (b - a) / 2) : Manifold.pathELength I γ a b < ENNReal.ofReal (b - a)

If the squared Riemannian speed of a curve is integrable on [a, b], where a < b, and its energy over [a, b] is less than (b - a) / 2, the energy of a unit-speed curve, then its length over [a, b] is less than b - a.

theorem ContMDiffOn.pathELength_le_ofReal_sqrt_energy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ s) (hs : UniqueMDiff[s]) {a b : ℝ} (hab : a ≤ b) (hsub : Set.Icc a b ⊆ s) : Manifold.pathELength I γ a b ≤ ENNReal.ofReal √(2 * (b - a) * TauCeti.Manifold.energy I γ a b)

Length is controlled by energy. The Riemannian length L of a C¹ curve over a compact interval [a, b] inside its parameter set and its energy E satisfy L ^ 2 ≤ 2 * (b - a) * E. This is the Cauchy–Schwarz inequality for the speed ‖γ'‖ on [a, b].

theorem ContMDiffOn.pathELength_lt_of_energy_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ s) (hs : UniqueMDiff[s]) {a b : ℝ} (hab : a < b) (hsub : Set.Icc a b ⊆ s) (hE : TauCeti.Manifold.energy I γ a b < (b - a) / 2) : Manifold.pathELength I γ a b < ENNReal.ofReal (b - a)

If the energy of a C¹ curve over a compact interval [a, b] inside its parameter set, where a < b, is less than (b - a) / 2, then its length over [a, b] is less than b - a.

Unit-speed reparametrization

theorem TauCeti.Manifold.exists_unit_speed_reparametrization_Icc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {a b : ℝ} (hab : a < b) (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc a b)) (hreg : ∀ t ∈ Set.Icc a b, curveVelocityWithin I γ (Set.Icc a b) t ≠ 0) : ∃ (ψ : ℝ → ℝ), (∀ t ∈ Set.Icc a b, ψ (∫ (r : ℝ) in a..t, ‖curveVelocityWithin I γ (Set.Icc a b) r‖) = t) ∧ (∀ s ∈ Set.Icc 0 (∫ (r : ℝ) in a..b, ‖curveVelocityWithin I γ (Set.Icc a b) r‖), ∫ (r : ℝ) in a..ψ s, ‖curveVelocityWithin I γ (Set.Icc a b) r‖ = s) ∧ (∀ s ∈ Set.Icc 0 (∫ (r : ℝ) in a..b, ‖curveVelocityWithin I γ (Set.Icc a b) r‖), ψ s ∈ Set.Icc a b) ∧ StrictMonoOn ψ (Set.Icc 0 (∫ (r : ℝ) in a..b, ‖curveVelocityWithin I γ (Set.Icc a b) r‖)) ∧ ContDiff ℝ 1 ψ ∧ ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 (γ ∘ ψ) (Set.Icc 0 (∫ (r : ℝ) in a..b, ‖curveVelocityWithin I γ (Set.Icc a b) r‖)) ∧ (γ ∘ ψ) 0 = γ a ∧ (γ ∘ ψ) (∫ (r : ℝ) in a..b, ‖curveVelocityWithin I γ (Set.Icc a b) r‖) = γ b ∧ (∀ s ∈ Set.Icc 0 (∫ (r : ℝ) in a..b, ‖curveVelocityWithin I γ (Set.Icc a b) r‖), ‖curveVelocityWithin I (γ ∘ ψ) (Set.Icc 0 (∫ (r : ℝ) in a..b, ‖curveVelocityWithin I γ (Set.Icc a b) r‖)) s‖ = 1) ∧ Manifold.pathELength I (γ ∘ ψ) 0 (∫ (r : ℝ) in a..b, ‖curveVelocityWithin I γ (Set.Icc a b) r‖) = Manifold.pathELength I γ a b ∧ ∫ (r : ℝ) in a..b, ‖curveVelocityWithin I γ (Set.Icc a b) r‖ = (Manifold.pathELength I γ a b).toReal

Arc-length reparametrization of a regular curve on a closed interval. Let γ be C¹ within [a, b], where a < b, with nonzero velocity within [a, b] at every point of [a, b]. There is a globally C¹ function ψ, increasing from [0, ∫_a^b ‖γ'(t)‖ dt] onto [a, b], which inverts accumulated length. The curve γ ∘ ψ has the same endpoints and path length as γ, and its velocity within its parameter interval has norm one throughout that interval. The accumulated-speed endpoint is identified with the real value of Manifold.pathELength.

Unlike exists_unit_speed_reparametrization, nothing is assumed about γ outside [a, b], and all velocities are read within the parameter interval. The interval is nondegenerate because a velocity within a singleton carries no information.

theorem TauCeti.Manifold.exists_unit_speed_reparametrization {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {J : Set ℝ} (hJ : IsOpen J) (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ J) {a b : ℝ} (hab : a ≤ b) (hsub : Set.Icc a b ⊆ J) (hreg : ∀ t ∈ Set.Icc a b, curveVelocity I γ t ≠ 0) : ∃ (ψ : ℝ → ℝ), (∀ t ∈ Set.Icc a b, ψ (∫ (r : ℝ) in a..t, ‖curveVelocity I γ r‖) = t) ∧ (∀ s ∈ Set.Icc 0 (∫ (r : ℝ) in a..b, ‖curveVelocity I γ r‖), ∫ (r : ℝ) in a..ψ s, ‖curveVelocity I γ r‖ = s) ∧ (∀ s ∈ Set.Icc 0 (∫ (r : ℝ) in a..b, ‖curveVelocity I γ r‖), ψ s ∈ Set.Icc a b) ∧ StrictMonoOn ψ (Set.Icc 0 (∫ (r : ℝ) in a..b, ‖curveVelocity I γ r‖)) ∧ ContDiffOn ℝ 1 ψ (Set.Icc 0 (∫ (r : ℝ) in a..b, ‖curveVelocity I γ r‖)) ∧ ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 (γ ∘ ψ) (Set.Icc 0 (∫ (r : ℝ) in a..b, ‖curveVelocity I γ r‖)) ∧ (γ ∘ ψ) 0 = γ a ∧ (γ ∘ ψ) (∫ (r : ℝ) in a..b, ‖curveVelocity I γ r‖) = γ b ∧ (∀ s ∈ Set.Icc 0 (∫ (r : ℝ) in a..b, ‖curveVelocity I γ r‖), ‖curveVelocity I (γ ∘ ψ) s‖ = 1) ∧ Manifold.pathELength I (γ ∘ ψ) 0 (∫ (r : ℝ) in a..b, ‖curveVelocity I γ r‖) = Manifold.pathELength I γ a b ∧ ∫ (r : ℝ) in a..b, ‖curveVelocity I γ r‖ = (Manifold.pathELength I γ a b).toReal

Arc-length reparametrization of a regular curve. Let γ be C¹ on an open set J containing [a, b], with nonzero velocity along [a, b]. There is an increasing C¹ function ψ from [0, ∫_a^b ‖γ'(t)‖ dt] to [a, b] which inverts accumulated length. The curve γ ∘ ψ has the same endpoints and path length as γ, and its velocity has norm one throughout its parameter interval. The accumulated-speed endpoint is identified with the real value of Manifold.pathELength.

The case a = b is included: the new parameter interval is then the singleton {0}. For a curve which is only C¹ within [a, b], see exists_unit_speed_reparametrization_Icc.