Broken radial geodesics through the base point are not minimizing

Let v and w be tangent vectors at p in the natural domain of the exponential map. Following the radial geodesic from exp_p v back to p and then the radial geodesic from p out to exp_p w gives a path of length ‖v‖ + ‖w‖. When v and w are nonzero and do not point in opposite directions, this path has a genuine corner at p, and it is not minimizing:

edist (exp_p v) (exp_p w) < ‖v‖ + ‖w‖.

This strict inequality supplies the local rigidity needed to extend a minimizing geodesic segment in the proof that an everywhere-defined exponential map yields minimizing geodesics: a distance-realizing path formed from radial legs through a point must leave that point in the direction in which it arrived.

Main results

• TauCeti.Manifold.eventually_edist_riemannianExp_smul_le: near the origin, exp_p lengthens the chord from t • v to t • w by at most a factor arbitrarily close to 1.
• TauCeti.Manifold.edist_riemannianExp_lt_enorm_add_enorm and TauCeti.Manifold.dist_riemannianExp_lt_norm_add_norm: a broken radial path through p whose legs are not opposite is strictly longer than the distance between its endpoints.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 7, §2, proof of Thm. 2.8, the step showing that the minimizing direction propagates.
• J. M. Lee, Introduction to Riemannian Manifolds, Springer, 2018, Ch. 6, proof of Thm. 6.19.

theorem TauCeti.Manifold.eventually_edist_riemannianExp_smul_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] [I.Boundaryless] {M : Type u_3} [EMetricSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [IsRiemannianManifold I M] (p : M) (v w : TangentSpace I p) {η : ℝ} (hη : 0 < η) : ∀ᶠ (t : ℝ) in nhdsWithin 0 (Set.Ioi 0), edist (riemannianExp I M p (t • v)) (riemannianExp I M p (t • w)) ≤ ENNReal.ofReal (t * (‖w - v‖ + η))

Near the origin the exponential map lengthens chords by at most a factor close to 1: for every η > 0, if t > 0 is small enough then exp_p (t • v) and exp_p (t • w) are at distance at most t * (‖w - v‖ + η).

theorem TauCeti.Manifold.edist_riemannianExp_lt_enorm_add_enorm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] [I.Boundaryless] {M : Type u_3} [EMetricSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [IsRiemannianManifold I M] {p : M} {v w : TangentSpace I p} (hv : v ∈ expDomain I M p) (hw : w ∈ expDomain I M p) (hvw : ¬SameRay ℝ v (-w)) : edist (riemannianExp I M p v) (riemannianExp I M p w) < ‖v‖ₑ + ‖w‖ₑ

A broken radial path through the base point is not minimizing. Let v and w lie in the natural domain of exp_p, with v and -w not on a common ray: both are nonzero and they do not point in opposite directions. Then exp_p v and exp_p w are at distance strictly less than ‖v‖ + ‖w‖, the length of the path which follows the radial geodesic from exp_p v back to p and then the radial geodesic from p to exp_p w.

theorem TauCeti.Manifold.dist_riemannianExp_lt_norm_add_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] [I.Boundaryless] {M : Type u_3} [MetricSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [IsRiemannianManifold I M] {p : M} {v w : TangentSpace I p} (hv : v ∈ expDomain I M p) (hw : w ∈ expDomain I M p) (hvw : ¬SameRay ℝ v (-w)) : dist (riemannianExp I M p v) (riemannianExp I M p w) < ‖v‖ + ‖w‖

A broken radial path through the base point whose legs are not opposite is strictly longer than the distance between its endpoints; see edist_riemannianExp_lt_enorm_add_enorm.