Hopf–Rinow theorem

DefinitionConstant-speed geodesic in a metric space#✓fully proved

Let \(M\) be an extended metric space with distance \(d\). A path \(\gamma : \mathbb{R} \to M\) is a constant-speed geodesic if there is a real number \(c \ge 0\) such that every \(t_0 \in \mathbb{R}\) has a \(\delta > 0\) with \(d(\gamma(s), \gamma(t)) = c\,|t - s|\) for all real \(s, t\) with \(|s - t_0| < \delta\) and \(|t - t_0| < \delta\).

def IsGeodesic {M : Type*} [EMetricSpace M] (γ : ℝ → M) : Prop :=
  ∃ c : NNReal, ∀ t₀ : ℝ, ∃ δ > (0 : ℝ),
    ∀ s t : ℝ, |s - t₀| < δ → |t - t₀| < δ →
      edist (γ s) (γ t) = (c : ℝ≥0∞) * ENNReal.ofReal |t - s|

Used by 1

Used byGeodesically complete metric space

DefinitionGeodesically complete metric space#✓fully proved

An extended metric space \(M\) with distance \(d\) is geodesically complete if the following holds for all real numbers \(a < b\) and every path \(\gamma : \mathbb{R} \to M\). Suppose there is a real \(c \ge 0\) such that every \(t_0 \in (a, b)\) has a \(\delta > 0\) with \(d(\gamma(s), \gamma(t)) = c\,|t - s|\) for all \(s, t\) in the interval \((a, b) \cap (t_0 - \delta, t_0 + \delta)\). Then there is a constant-speed geodesic \(\tilde\gamma : \mathbb{R} \to M\) with \(\tilde\gamma(t) = \gamma(t)\) for all \(t \in (a, b)\).

def IsGeodesicallyComplete (M : Type*) [EMetricSpace M] : Prop :=
  ∀ (a b : ℝ) (γ : ℝ → M), a < b →
    (∃ c : NNReal, ∀ t₀ ∈ Set.Ioo a b, ∃ δ > (0 : ℝ),
      ∀ s t : ℝ,
        s ∈ Set.Ioo (max a (t₀ - δ)) (min b (t₀ + δ)) →
        t ∈ Set.Ioo (max a (t₀ - δ)) (min b (t₀ + δ)) →
        edist (γ s) (γ t) = (c : ℝ≥0∞) * ENNReal.ofReal |t - s|) →
    ∃ γext : ℝ → M, IsGeodesic γext ∧ ∀ t ∈ Set.Ioo a b, γext t = γ t

Uses 1 · Used by 1

Statement usesConstant-speed geodesic in a metric space

Used byHopf–Rinow theorem

TheoremHopf–Rinow theorem#●ready to prove

Let \(M\) be a connected, locally compact smooth manifold without boundary, modelled on a finite-dimensional real normed space, with a smooth Riemannian metric whose Riemannian distance is the (extended) distance of \(M\). Then \(M\) is geodesically complete if and only if \(M\) is complete for its distance.

public theorem_wanted 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] :
    IsGeodesicallyComplete M ↔ CompleteSpace M

Sources

• 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). Problem hopf_rinow of the lean-eval benchmark.

Uses 1

Statement usesGeodesically complete metric space

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.