Smooth paths with prescribed Riemannian path length

For a C¹ path on [0, 1], there exists a globally C¹ path that is constant near both endpoints, has the same endpoints, and has exactly the same Manifold.pathELength. For two C¹ paths with a common endpoint, there likewise exists a globally C¹ path between their outer endpoints whose length is the sum of their lengths. These are the basic existential properties needed to compare piecewise-C¹ and C¹ definitions of Riemannian distance.

The reparametrizations do not introduce new points: the smoothed path stays in the image of the original path, and a smoothed concatenation stays in the union of the two original images. This range control allows local length estimates to be applied after smoothing a path inside a fixed open set.

A path on an arbitrary compact interval can first be reparametrized affinely onto [0, 1] without changing its endpoints or length.

The construction uses Mathlib's Real.smoothTransition and Manifold.pathELength_comp_of_monotoneOn. No new notion of path length is introduced.

Main results

• TauCeti.exists_contMDiff_pathELength_eq: obtain a globally C¹ path, constant near its endpoints, with the same endpoints, length, and image containment as a given C¹ path.
• TauCeti.Manifold.exists_contMDiff_pathELength_eq_of_le: reparametrize a C¹ path from an arbitrary compact interval onto [0, 1], preserving its endpoints and length.
• TauCeti.exists_contMDiff_pathELength_eq_add: obtain a globally C¹ path between the outer endpoints of two compatible C¹ paths, with length equal to the sum of their lengths.
• TauCeti.Manifold.pathELength_lineMap: the straight segment between two points of an inner product space has length equal to the norm distance between them.

References

• M. P. do Carmo, Riemannian Geometry, Chapter 1, Definition 2.9 and Chapter 7, Section 2.
• The Hopf--Rinow roadmap, Layer 0, "Corner smoothing and the piecewise-C¹ comparison".

theorem TauCeti.exists_contMDiff_pathELength_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] [(x : M) → ENorm (TangentSpace I x)] [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)] {γ : ℝ → M} (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc 0 1)) : ∃ (η : ℝ → M), ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 η ∧ η 0 = γ 0 ∧ η 1 = γ 1 ∧ Manifold.pathELength I η 0 1 = Manifold.pathELength I γ 0 1 ∧ (η =ᶠ[nhds 0] fun (x : ℝ) => γ 0) ∧ (η =ᶠ[nhds 1] fun (x : ℝ) => γ 1) ∧ Set.MapsTo η (Set.Icc 0 1) (γ '' Set.Icc 0 1)

A C¹ path on [0, 1] admits a globally C¹ path which is constant near both endpoints, has the same endpoints and length, and stays in the image of the original path.

theorem TauCeti.Manifold.exists_contMDiff_pathELength_eq_of_le {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] [(x : M) → ENorm (TangentSpace I x)] [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)] {γ : ℝ → M} {a b : ℝ} (hab : a ≤ b) (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc a b)) : ∃ (η : ℝ → M), ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 η ∧ η 0 = γ a ∧ η 1 = γ b ∧ Manifold.pathELength I η 0 1 = Manifold.pathELength I γ a b ∧ Set.MapsTo η (Set.Icc 0 1) (γ '' Set.Icc a b)

A C¹ path on a compact interval admits a globally C¹ path on [0, 1] with the same endpoints and length, whose image stays in the original path's image. This is the single-piece case of corner smoothing; the reparametrization is affine, so it changes neither the endpoints nor the length.

theorem TauCeti.exists_contMDiff_pathELength_eq_add {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] [(x : M) → ENorm (TangentSpace I x)] [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)] {γ₁ γ₂ : ℝ → M} (hγ₁ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ₁ (Set.Icc 0 1)) (hγ₂ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ₂ (Set.Icc 0 1)) (h₁₂ : γ₁ 1 = γ₂ 0) : ∃ (η : ℝ → M), ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 η ∧ η 0 = γ₁ 0 ∧ η 1 = γ₂ 1 ∧ Manifold.pathELength I η 0 1 = Manifold.pathELength I γ₁ 0 1 + Manifold.pathELength I γ₂ 0 1 ∧ (η =ᶠ[nhds 0] fun (x : ℝ) => γ₁ 0) ∧ (η =ᶠ[nhds 1] fun (x : ℝ) => γ₂ 1) ∧ Set.MapsTo η (Set.Icc 0 1) (γ₁ '' Set.Icc 0 1 ∪ γ₂ '' Set.Icc 0 1)

Given two C¹ paths on [0, 1] whose endpoints match, there is a globally C¹ path with their outer endpoints which is constant near those endpoints, whose length is the sum of the two original lengths, and whose image stays in the union of the two original path images.

@[simp]

theorem TauCeti.Manifold.pathELength_lineMap {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) : Manifold.pathELength (modelWithCornersSelf ℝ F) (⇑(ContinuousAffineMap.lineMap x y)) 0 1 = ‖x - y‖ₑ

The straight segment between two points of an inner product space has length equal to the norm distance between them.