Radial minimization inside a normal neighbourhood

The radial geodesic from the centre of a normal neighbourhood to one of its points minimizes Riemannian length among the C¹ curves that stay in that neighbourhood. The Gauss lemma gives a lower bound by the change in the norm of the logarithm; the radial geodesic attains that bound. Corner smoothing extends the comparison to piecewise C¹ competitors without changing their endpoints or length while keeping them inside the normal neighbourhood.

This local comparison is the input for the escape argument that turns radial length into the Riemannian distance, whose infimum ranges over paths that may leave the normal neighbourhood.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 3, §3.
• J. M. Lee, Introduction to Riemannian Manifolds, Springer, 2018, Ch. 6.

theorem TauCeti.Manifold.IsNormalDomain.pathELength_riemannianExp_smul_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [EMetricSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [I.Boundaryless] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {p : M} {U : Set (TangentSpace I p)} (h : IsNormalDomain I M p U) {v : TangentSpace I p} (hv : v ∈ U) {γ : ℝ → M} {a b : ℝ} (hab : a ≤ b) (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc a b)) (hγU : Set.MapsTo γ (Set.Icc a b) (riemannianExp I M p '' U)) (hγa : γ a = p) (hγb : γ b = riemannianExp I M p v) : Manifold.pathELength I (fun (t : ℝ) => riemannianExp I M p (t • v)) 0 1 ≤ Manifold.pathELength I γ a b

A radial geodesic minimizes length inside a normal neighbourhood. Any C¹ curve from p to exp_p v that remains in the image of a normal domain containing v has length at least that of the radial geodesic.

theorem TauCeti.Manifold.IsNormalDomain.pathELength_riemannianExp_smul_le_of_piecewise {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [EMetricSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [I.Boundaryless] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {p : M} {U : Set (TangentSpace I p)} (h : IsNormalDomain I M p U) {v : TangentSpace I p} (hv : v ∈ U) {γ : ℝ → M} {a b : ℝ} (hγ : IsPiecewiseContMDiffOn I 1 γ a b) (hγU : Set.MapsTo γ (Set.Icc a b) (riemannianExp I M p '' U)) (hγa : γ a = p) (hγb : γ b = riemannianExp I M p v) : Manifold.pathELength I (fun (t : ℝ) => riemannianExp I M p (t • v)) 0 1 ≤ Manifold.pathELength I γ a b

A radial geodesic also minimizes against piecewise C¹ competitors in the normal neighbourhood, including broken paths with finitely many corners. The competitor may have any nondegenerate compact parameter interval.