Metric completeness gives geodesic completeness

A maximal geodesic travels at constant speed, so on its maximal interval it is a Lipschitz curve for the Riemannian distance. If that interval had a finite endpoint, the image of the curve would therefore be totally bounded, hence relatively compact once the manifold is metrically complete. This contradicts the escape lemma for geodesics, eventually_notMem_nhdsLT_maximalGeodesic, so no such endpoint exists and every geodesic is defined for all time. The same Lipschitz bound, read between the parameters 0 and 1, says that the exponential map does not increase the distance from the base point: dist p (exp_p v) ≤ ‖v‖.

Main results

• TauCeti.Manifold.lipschitzOnWith_maximalGeodesic: consequently it is ‖v‖-Lipschitz there.
• TauCeti.Manifold.edist_riemannianExp_le and TauCeti.Manifold.dist_riemannianExp_le: the distance from p to exp_p v is at most ‖v‖.
• TauCeti.Manifold.isGeodesicallyCompleteAt_of_completeSpace: a complete Riemannian manifold is geodesically complete at every point, with TauCeti.Manifold.isGeodesicCurveOnFrom_maximalGeodesic_univ the resulting all-time geodesic and TauCeti.Manifold.expDomain_eq_univ_of_completeSpace the resulting everywhere-defined exponential map.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 7, §2, Thm. 2.8, the implication from assertion (c), metric completeness, to assertion (d), geodesic completeness.
• J. M. Lee, Introduction to Riemannian Manifolds, Springer, 2018, Ch. 6, Thm. 6.19.

Lipschitz bound

theorem TauCeti.Manifold.lipschitzOnWith_maximalGeodesic {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} {v : TangentSpace I p} [IsRiemannianManifold I M] : LipschitzOnWith ‖v‖₊ (maximalGeodesic I M p v) (geodesicInterval I M p v)

A maximal geodesic is Lipschitz on its maximal interval, with its constant speed as Lipschitz constant.

The distance bound for the exponential map

theorem TauCeti.Manifold.edist_riemannianExp_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] [IsRiemannianManifold I M] (p : M) (v : TangentSpace I p) : edist p (riemannianExp I M p v) ≤ ‖v‖ₑ

The exponential map does not increase the distance from the base point. The extended distance from p to exp_p v is at most ‖v‖ₑ, for every tangent vector v at p.

theorem TauCeti.Manifold.dist_riemannianExp_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_4} [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 : TangentSpace I p) : dist p (riemannianExp I M p v) ≤ ‖v‖

The distance from p to exp_p v is at most ‖v‖; see edist_riemannianExp_le.

Completeness

theorem TauCeti.Manifold.isGeodesicallyCompleteAt_of_completeSpace {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] [IsRiemannianManifold I M] [CompleteSpace M] (p : M) : IsGeodesicallyCompleteAt I M p

Metric completeness implies geodesic completeness. In a Riemannian manifold which is complete for its Riemannian distance, every maximal geodesic is defined for all time. This is the implication from assertion (c) to assertion (d) of do Carmo's Hopf–Rinow theorem.

theorem TauCeti.Manifold.isGeodesicCurveOnFrom_maximalGeodesic_univ {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] [IsRiemannianManifold I M] [CompleteSpace M] (p : M) (v : TangentSpace I p) : IsGeodesicCurveOnFrom I (maximalGeodesic I M p v) Set.univ p v

In a complete Riemannian manifold the maximal geodesic with initial data (p, v) is a geodesic on the whole real line.

theorem TauCeti.Manifold.expDomain_eq_univ_of_completeSpace {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] [IsRiemannianManifold I M] [CompleteSpace M] (p : M) : expDomain I M p = Set.univ

The exponential map of a complete Riemannian manifold is everywhere defined, its domain being the whole tangent space at every point.