Minimizing geodesics from an everywhere-defined exponential map

Let M be a Riemannian manifold whose distance is the Riemannian distance, and suppose that the exponential map at p is defined on all of T_p M. Then every point q is reached from p by a minimizing geodesic: there is a tangent vector v with exp_p v = q and ‖v‖ = dist p q, so that the geodesic t ↦ exp_p (t • v) on [0, 1] joins p to q, has length dist p q, and each of its subsegments realizes the distance between its endpoints.

Combined with properSpace_of_expDomain_eq_univ_of_exists_riemannianExp_eq_and_norm_le_dist, this shows that an everywhere-defined exponential map at a single point makes the manifold proper, and, through expDomain_eq_univ_of_completeSpace, that a complete Riemannian manifold is proper.

Main results

In the namespace TauCeti.Manifold:

• exists_riemannianExp_eq_and_norm_eq_dist: if exp_p is everywhere defined, every point is exp_p v for a tangent vector v with ‖v‖ = dist p q.
• dist_riemannianExp_smul_riemannianExp_smul: along such a minimizing initial velocity, the radial geodesic on [0, 1] travels at constant speed dist p q in the metric sense.
• dist_riemannianExp_smul_riemannianExp_smul_of_mem_Icc: the same constant metric speed for s, t ∈ [0, a] along a minimizing vector a • v.
• dist_riemannianExp_smul_eq_norm and dist_riemannianExp_smul_eq_norm_of_le: shorter radial segments in a minimizing direction are minimizing.
• isClosed_setOf_dist_riemannianExp_eq_norm: if exp_p is everywhere defined, the tangent vectors v at p with dist p (exp_p v) = ‖v‖ form a closed set.
• exists_isGeodesicCurveOn_Icc_pathELength_eq_edist: a minimizing geodesic segment joins p to every point, and each of its subsegments realizes the distance between its endpoints.
• properSpace_of_expDomain_eq_univ: an everywhere-defined exponential map at one point makes the manifold proper.
• properSpace_of_completeSpace: a complete Riemannian manifold is proper.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 7, §2, Thm. 2.8, the implication from assertion (a) to assertion (f), and the implications (a) ⇒ (b) and (c) ⇒ (b).
• J. M. Lee, Introduction to Riemannian Manifolds, Springer, 2018, Ch. 6, Lemma 6.18 and Thm. 6.19.

theorem TauCeti.Manifold.exists_riemannianExp_eq_and_norm_eq_dist {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [MetricSpace 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] [IsRiemannianManifold I M] {p : M} (ha : expDomain I M p = Set.univ) (q : M) : ∃ (v : TangentSpace I p), riemannianExp I M p v = q ∧ ‖v‖ = dist p q

An everywhere-defined exponential map reaches every point minimally. If the exponential map at p is defined on all of T_p M, then every point q is exp_p v for a tangent vector v with ‖v‖ = dist p q.

theorem TauCeti.Manifold.isClosed_setOf_dist_riemannianExp_eq_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [MetricSpace 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} (ha : expDomain I M p = Set.univ) : IsClosed {v : TangentSpace I p | dist p (riemannianExp I M p v) = ‖v‖}

If the exponential map at p is defined on all of T_p M, the tangent vectors v at p with dist p (exp_p v) = ‖v‖ form a closed set.

theorem TauCeti.Manifold.dist_riemannianExp_smul_riemannianExp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [MetricSpace 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] [IsRiemannianManifold I M] {p : M} {v : TangentSpace I p} (hmin : ‖v‖ ≤ dist p (riemannianExp I M p v)) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) : dist (riemannianExp I M p (s • v)) (riemannianExp I M p (t • v)) = |s - t| * ‖v‖

Minimizing radial geodesics travel at constant metric speed. If ‖v‖ ≤ dist p (exp_p v) (so that v lies in the domain of exp_p and equality holds, by mem_expDomain_of_norm_le_dist and dist_riemannianExp_le), then for all s, t ∈ [0, 1] the points exp_p (s • v) and exp_p (t • v) are at distance |s - t| * ‖v‖.

theorem TauCeti.Manifold.dist_riemannianExp_smul_eq_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [MetricSpace 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] [IsRiemannianManifold I M] {p : M} {v : TangentSpace I p} (hmin : dist p (riemannianExp I M p v) = ‖v‖) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : dist p (riemannianExp I M p (t • v)) = ‖t • v‖

Subsegments of minimizing radial segments are minimizing. If dist p (exp_p v) = ‖v‖, then dist p (exp_p (t • v)) = ‖t • v‖ for every t ∈ [0, 1].

theorem TauCeti.Manifold.dist_riemannianExp_smul_riemannianExp_smul_of_mem_Icc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [MetricSpace 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] [IsRiemannianManifold I M] {p : M} {v : TangentSpace I p} {a s t : ℝ} (hmin : dist p (riemannianExp I M p (a • v)) = ‖a • v‖) (hs : s ∈ Set.Icc 0 a) (ht : t ∈ Set.Icc 0 a) : dist (riemannianExp I M p (s • v)) (riemannianExp I M p (t • v)) = |s - t| * ‖v‖

Minimizing radial geodesics travel at constant metric speed, rescaled form. If dist p (exp_p (a • v)) = ‖a • v‖, then for all s, t ∈ [0, a] the points exp_p (s • v) and exp_p (t • v) are at distance |s - t| * ‖v‖.

theorem TauCeti.Manifold.dist_riemannianExp_smul_eq_norm_of_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [MetricSpace 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] [IsRiemannianManifold I M] {p : M} {v : TangentSpace I p} {a b : ℝ} (hmin : dist p (riemannianExp I M p (a • v)) = ‖a • v‖) (hb : 0 ≤ b) (hba : b ≤ a) : dist p (riemannianExp I M p (b • v)) = ‖b • v‖

Shorter radial segments in a minimizing direction are minimizing. If dist p (exp_p (a • v)) = ‖a • v‖, then dist p (exp_p (b • v)) = ‖b • v‖ for every b with 0 ≤ b ≤ a.

theorem TauCeti.Manifold.exists_isGeodesicCurveOn_Icc_pathELength_eq_edist {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [MetricSpace 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] [IsRiemannianManifold I M] {p : M} (ha : expDomain I M p = Set.univ) (q : M) : ∃ (γ : ℝ → M), IsGeodesicCurveOn I γ (Set.Icc 0 1) ∧ γ 0 = p ∧ γ 1 = q ∧ Manifold.pathELength I γ 0 1 = edist p q ∧ ∀ s ∈ Set.Icc 0 1, ∀ t ∈ Set.Icc 0 1, s ≤ t → Manifold.pathELength I γ s t = edist (γ s) (γ t)

An everywhere-defined exponential map yields minimizing geodesics. If the exponential map at p is defined on all of T_p M, then every point q is joined to p by a geodesic segment γ on [0, 1] whose length is the distance from p to q; moreover each of its subsegments realizes the distance between its endpoints.

theorem TauCeti.Manifold.properSpace_of_expDomain_eq_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [MetricSpace 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] [IsRiemannianManifold I M] {p : M} (ha : expDomain I M p = Set.univ) : ProperSpace M

An everywhere-defined exponential map makes the manifold proper. If the exponential map at a single point p is defined on all of T_p M, every closed bounded subset of M is compact.

theorem TauCeti.Manifold.properSpace_of_completeSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [MetricSpace 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] [IsRiemannianManifold I M] [CompleteSpace M] : ProperSpace M

A complete Riemannian manifold is proper: its closed bounded subsets are compact. The model I cannot be inferred from the conclusion, so it is an explicit argument.