Hopf–Rinow theorem

hopf_rinow

Submitter: Kim Morrison.

Notes: For a connected, finite-dimensional, smooth Riemannian manifold M that is also locally compact, metric completeness and geodesic completeness are equivalent. §93 of Knill's 'Some Fundamental Theorems in Mathematics'. The file ships IsGeodesic (a path with locally linear edist — a metric formulation of affinely parametrised local minimising geodesics, avoiding any Levi-Civita / connection infrastructure) and IsGeodesicallyComplete (every geodesic on a bounded open interval extends to all of ℝ).

Source: H. Hopf and W. Rinow, *Ueber den Begriff der vollständigen differentialgeometrischen Fläche*, Comment. Math. Helv. 3 (1931), 209-225. Listed as §93 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Standard Hopf–Rinow proof. Metric ⇒ geodesic completeness: a constant-speed geodesic γ : (a, b) → M is uniformly Cauchy as t → b⁻ because edist (γ s) (γ t) = c · |s − t|; the limit exists by metric completeness, and the geodesic ODE extends past the limit point using local existence of geodesics (Picard–Lindelöf on the tangent bundle). Geodesic ⇒ metric completeness: the central Hopf–Rinow lemma shows that under the smooth-Riemannian-and-locally-compact hypotheses, closed bounded subsets of M are compact (Heine–Borel). A Cauchy sequence is bounded, hence contained in a compact set, hence convergent.

theorem declaration uses `sorry`hopf_rinow {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E]
    {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H)
    [I.Boundaryless]
    (M : Type*) [EMetricSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
    [Bundle.RiemannianBundle (fun x : M => TangentSpace I x)]
    [IsContMDiffRiemannianBundle I ∞ E (fun x : M => TangentSpace I x)]
    [IsContinuousRiemannianBundle E (fun x : M => TangentSpace I x)]
    [IsRiemannianManifold I M]
    [LocallyCompactSpace M] [ConnectedSpace M] :
    LeanEval.Geometry.IsGeodesicallyComplete M ↔ CompleteSpace M := byE:Type u_1inst✝¹³:NormedAddCommGroup Einst✝¹²:NormedSpace ℝ Einst✝¹¹:FiniteDimensional ℝ EH:Type u_2inst✝¹⁰:TopologicalSpace HI:ModelWithCorners ℝ E Hinst✝⁹:I.BoundarylessM:Type u_3inst✝⁸:EMetricSpace Minst✝⁷:ChartedSpace H Minst✝⁶:IsManifold I ∞ Minst✝⁵:RiemannianBundle fun x => TangentSpace I xinst✝⁴:IsContMDiffRiemannianBundle I ∞ E fun x => TangentSpace I xinst✝³:IsContinuousRiemannianBundle E fun x => TangentSpace I xinst✝²:IsRiemannianManifold I Minst✝¹:LocallyCompactSpace Minst✝:ConnectedSpace M⊢ IsGeodesicallyComplete M ↔ CompleteSpace M
  sorryAll goals completed! 🐙

Solved by

Not yet solved.