The piecewise smooth description of the Riemannian distance

do Carmo defines the distance between two points of a Riemannian manifold as the infimum of the lengths of the piecewise C¹ paths joining them, whereas Mathlib's Manifold.riemannianEDist is the infimum over C¹ paths only. This file proves that the two infima agree.

The bridge is corner smoothing. Each piece of a piecewise C¹ path is first reparametrized affinely onto [0, 1], which changes neither its endpoints nor its length, and then flattened near its endpoints by TauCeti.exists_contMDiff_pathELength_eq; the flattened pieces can be concatenated with TauCeti.exists_contMDiff_pathELength_eq_add while staying globally C¹. Iterating over the partition replaces a broken path by a C¹ path with the same endpoints and exactly the same length, so neither infimum can be smaller than the other.

The explicit-partition induction used for the subinterval comparison is adapted from the Apache-2.0 do Carmo formalization at revision 24f32e4d600878bfaac6bc2f2f9324175571c321.

Main results

• TauCeti.Manifold.IsPiecewiseContMDiffOn.exists_contMDiff_pathELength_eq: corner smoothing, every piecewise C¹ path has a globally C¹ path on [0, 1] with the same endpoints and the same length, whose image stays in the original path's image.
• TauCeti.Manifold.IsPiecewiseContMDiffOn.exists_contMDiff_pathELength_eq_of_mapsTo: smooth a piecewise path while keeping it inside any set containing the original path.
• TauCeti.Manifold.IsPiecewiseContMDiffOn.riemannianEDist_le_pathELength: a piecewise C¹ path bounds the Riemannian extended distance between its endpoints.
• TauCeti.Manifold.IsPiecewiseContMDiffOn.riemannianEDist_le_pathELength_of_subset: the same bound between any two ordered parameters in the path's interval, and TauCeti.Manifold.IsPiecewiseContMDiffOn.edist_le_pathELength_of_subset, its form for the ambient extended distance of a Riemannian manifold.
• TauCeti.Manifold.riemannianEDist_eq_iInf_pathELength_piecewise and TauCeti.Manifold.riemannianEDist_eq_iInf_pathELength_piecewise_zero_one: the piecewise C¹ infimum, over arbitrary parameter intervals and over [0, 1], is Manifold.riemannianEDist.

Only Mathlib's Manifold.pathELength and Manifold.riemannianEDist occur here; the piecewise formulation is exposed exclusively through the comparison theorems above, and no competing notion of length or distance is introduced.

References

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

theorem TauCeti.Manifold.IsPiecewiseContMDiffOn.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} {a b : ℝ} (h : IsPiecewiseContMDiffOn I 1 γ 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)

Corner smoothing. Every piecewise C¹ path admits a globally C¹ path on [0, 1] with the same endpoints and exactly the same Manifold.pathELength, whose image stays in the image of the original path.

This is the theorem which makes the piecewise C¹ and the C¹ descriptions of the Riemannian distance agree: a broken competitor can always be rounded off at its corners without gaining or losing length. The regularity index is 1 throughout because Manifold.riemannianEDist is an infimum over C¹ paths; the smoothed path is only claimed to be C¹, since the affine reparametrization of a piece is composed with a transition function which flattens it at the junctions.

theorem TauCeti.Manifold.IsPiecewiseContMDiffOn.exists_contMDiff_pathELength_eq_of_mapsTo {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 : ℝ} (h : IsPiecewiseContMDiffOn I 1 γ a b) {S : Set M} (hγS : Set.MapsTo γ (Set.Icc a b) S) : ∃ (η : ℝ → 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) S

Corner smoothing inside a set. If a piecewise C¹ path stays in S, it can be replaced by a globally C¹ path on [0, 1] with the same endpoints and length that also stays in S. No openness or other property of S is required.

theorem TauCeti.Manifold.IsPiecewiseContMDiffOn.riemannianEDist_le_pathELength {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 : ℝ} (h : IsPiecewiseContMDiffOn I 1 γ a b) : Manifold.riemannianEDist I (γ a) (γ b) ≤ Manifold.pathELength I γ a b

The Riemannian extended distance between the endpoints of a piecewise C¹ path is at most the length of that path. This is Mathlib's Manifold.riemannianEDist_le_pathELength for broken competitors.

theorem TauCeti.Manifold.IsPiecewiseContMDiffOn.riemannianEDist_le_pathELength_of_subset {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 : ℝ} (h : IsPiecewiseContMDiffOn I 1 γ a b) {s t : ℝ} (has : a ≤ s) (hst : s ≤ t) (htb : t ≤ b) : Manifold.riemannianEDist I (γ s) (γ t) ≤ Manifold.pathELength I γ s t

The Riemannian extended distance between two ordered points in the parameter interval of a piecewise C¹ path is at most the path length between those points.

theorem TauCeti.Manifold.riemannianEDist_eq_iInf_pathELength_piecewise {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)] (x y : M) : Manifold.riemannianEDist I x y = ⨅ (γ : ℝ → M), ⨅ (a : ℝ), ⨅ (b : ℝ), ⨅ (_ : IsPiecewiseContMDiffOn I 1 γ a b), ⨅ (_ : γ a = x), ⨅ (_ : γ b = y), Manifold.pathELength I γ a b

do Carmo's distance is Mathlib's distance. The Riemannian extended distance, defined by Mathlib as an infimum over C¹ paths, is also the infimum of the lengths of the piecewise C¹ paths joining the two points, over all parameter intervals.

The inequality ≥ holds because a C¹ path is piecewise C¹, and ≤ because corner smoothing turns a piecewise C¹ competitor into a C¹ one of the same length.

theorem TauCeti.Manifold.riemannianEDist_eq_iInf_pathELength_piecewise_zero_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] [(x : M) → ENorm (TangentSpace I x)] [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)] (x y : M) : Manifold.riemannianEDist I x y = ⨅ (γ : ℝ → M), ⨅ (_ : IsPiecewiseContMDiffOn I 1 γ 0 1), ⨅ (_ : γ 0 = x), ⨅ (_ : γ 1 = y), Manifold.pathELength I γ 0 1

The Riemannian extended distance is the infimum of the lengths of the piecewise C¹ paths joining the two points on the fixed parameter interval [0, 1]. Restricting to [0, 1] loses nothing, because corner smoothing sends a competitor on an arbitrary interval to one on [0, 1] with the same endpoints and the same length.

This is TauCeti.Manifold.riemannianEDist_eq_iInf_pathELength_piecewise specialized to the parameter interval [0, 1]: the two infima are compared directly, the [0, 1] competitors being a subfamily of the arbitrary-interval ones.

theorem TauCeti.Manifold.IsPiecewiseContMDiffOn.edist_le_pathELength_of_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [PseudoEMetricSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsRiemannianManifold I M] {γ : ℝ → M} {a b : ℝ} (h : IsPiecewiseContMDiffOn I 1 γ a b) {s t : ℝ} (has : a ≤ s) (hst : s ≤ t) (htb : t ≤ b) : edist (γ s) (γ t) ≤ Manifold.pathELength I γ s t

In a Riemannian manifold, the ambient extended distance between two ordered parameters of a piecewise C¹ path is at most the length of the path between them. This is TauCeti.Manifold.IsPiecewiseContMDiffOn.riemannianEDist_le_pathELength_of_subset read through IsRiemannianManifold.out.