The Hopf–Rinow theorem

Let M be a Riemannian manifold whose distance is the Riemannian distance, and let p ∈ M. The Hopf–Rinow theorem says that the following assertions are equivalent:

• (a) the exponential map exp_p is defined on all of T_p M;
• (b) M is a proper metric space: its closed bounded subsets are compact;
• (c) M is complete as a metric space;
• (d) M is geodesically complete: every maximal geodesic is defined for all time;
• (e) there is an increasing sequence of compact sets K n covering M such that dist p (q n) → ∞ along every sequence q with q n ∉ K n.

Each of them moreover implies that every point is joined to p by a minimizing geodesic segment, which is exists_isGeodesicCurveOn_Icc_pathELength_eq_edist.

The individual implications are proved elsewhere: (a) ⇒ (b) is properSpace_of_expDomain_eq_univ, (b) ⇒ (c) is Mathlib's complete_of_proper, (c) ⇒ (d) is isGeodesicallyCompleteAt_of_completeSpace, (d) ⇒ (a) is expDomain_eq_univ_iff, and (b) ⇔ (e) holds in every pseudometric space (TauCeti.properSpace_iff_exists_isCompact_monotone_iUnion_eq_univ_tendsto_dist). This file assembles them into a single List.TFAE statement and draws the consequence that completeness of the exponential map, or of the geodesics, at one point propagates to every point.

The statements are about an ordinary metric space M compatible with the Riemannian structure, [IsRiemannianManifold I M]. The finiteness of the Riemannian distance, which is what do Carmo's standing connectedness assumption supplies, is part of that structure, so no separate [ConnectedSpace M] hypothesis appears.

Main results

In the namespace TauCeti.Manifold:

• tfae_expDomain_eq_univ: the Hopf–Rinow theorem, the equivalence of (a)–(e).
• completeSpace_iff_isGeodesicallyCompleteAt: M is complete exactly when every geodesic leaving one given point is defined for all time.
• isGeodesicallyCompleteAt_iff_forall and expDomain_eq_univ_iff_forall: geodesic completeness at one point, equivalently an everywhere-defined exponential map at one point, propagates to every point.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 7, §2, Thm. 2.8.
• J. M. Lee, Introduction to Riemannian Manifolds, Springer, 2018, Ch. 6, Thm. 6.19.

theorem TauCeti.Manifold.tfae_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) : [expDomain I M p = Set.univ, ProperSpace M, CompleteSpace M, ∀ (q : M), IsGeodesicallyCompleteAt I M q, ∃ (K : ℕ → Set M), (∀ (n : ℕ), IsCompact (K n)) ∧ Monotone K ∧ ⋃ (n : ℕ), K n = Set.univ ∧ ∀ (q : ℕ → M), (∀ (n : ℕ), q n ∉ K n) → Filter.Tendsto (fun (n : ℕ) => dist p (q n)) Filter.atTop Filter.atTop].TFAE

The Hopf–Rinow theorem. For a point p of a Riemannian manifold M whose distance is the Riemannian distance, the following are equivalent: the exponential map at p is defined on all of T_p M; M is proper; M is complete; every maximal geodesic of M is defined for all time; and M has an increasing exhaustion by compact sets K n such that dist p (q n) → ∞ whenever q n ∉ K n for every n.

theorem TauCeti.Manifold.completeSpace_iff_isGeodesicallyCompleteAt {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) : CompleteSpace M ↔ IsGeodesicallyCompleteAt I M p

Geodesic completeness at one point is metric completeness. A Riemannian manifold M is complete exactly when every maximal geodesic leaving a given point p is defined for all time.

theorem TauCeti.Manifold.isGeodesicallyCompleteAt_iff_forall {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) : IsGeodesicallyCompleteAt I M p ↔ ∀ (q : M), IsGeodesicallyCompleteAt I M q

Geodesic completeness propagates from one point to every point. If every maximal geodesic leaving p is defined for all time, then so is every maximal geodesic of M.

theorem TauCeti.Manifold.expDomain_eq_univ_iff_forall {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) : expDomain I M p = Set.univ ↔ ∀ (q : M), expDomain I M q = Set.univ

An everywhere-defined exponential map at one point makes every exponential map everywhere defined. If exp_p is defined on all of T_p M, then exp_q is defined on all of T_q M for every point q.