Geodesics in metric spaces

DefinitionGeodesics of a given speed on a set of times#✓fully proved

Let \(X\) be a pseudo-extended metric space with extended distance \(d\), let \(\gamma : \mathbb{R} \to X\) be a curve, \(s \subseteq \mathbb{R}\) a set of times and \(c \ge 0\) a real number. The curve \(\gamma\) is a geodesic of speed \(c\) on \(s\) if every \(t \in s\) has some \(\varepsilon > 0\) such that \(d(\gamma(t_1), \gamma(t_2)) = c\,|t_1 - t_2|\) for all \(t_1, t_2 \in s\) with \(|t_1 - t| < \varepsilon\) and \(|t_2 - t| < \varepsilon\).

def IsGeodesicOnWithSpeed (γ : ℝ → X) (s : Set ℝ) (c : ℝ≥0) : Prop :=
  ∀ t ∈ s, ∃ ε > (0 : ℝ), ∀ t₁ ∈ s, ∀ t₂ ∈ s, |t₁ - t| < ε → |t₂ - t| < ε →
    edist (γ t₁) (γ t₂) = c * edist t₁ t₂

Used by 4

Used byConstant curves are geodesics · Straight lines are geodesics · Geodesic on a set of times · Straight lines are geodesics of constant speed

DefinitionGeodesic on a set of times#✓fully proved

Let \(X\) be a pseudo-extended metric space. A curve \(\gamma : \mathbb{R} \to X\) is a geodesic on a set of times \(s \subseteq \mathbb{R}\) if, for some real number \(c \ge 0\), it is a geodesic of speed \(c\) on \(s\).

On a Riemannian manifold without boundary, with its Riemannian distance, every Riemannian geodesic is a geodesic in this sense, and the piecewise \(C^1\) geodesics in this sense are the Riemannian geodesics.

def IsGeodesicOn (γ : ℝ → X) (s : Set ℝ) : Prop :=
  ∃ c : ℝ≥0, IsGeodesicOnWithSpeed γ s c

Uses 1 · Used by 1

Statement usesGeodesics of a given speed on a set of times

Used byGeodesics defined for all times

DefinitionGeodesics defined for all times#✓fully proved

Let \(X\) be a pseudo-extended metric space. A curve \(\gamma : \mathbb{R} \to X\) is a geodesic if it is a geodesic on the set of all times \(\mathbb{R}\).

def IsGeodesic (γ : ℝ → X) : Prop :=
  IsGeodesicOn γ univ

Uses 1 · Used by 5

Statement usesGeodesic on a set of times

Used byClosed geodesic · Constant curves are geodesics · Straight lines are geodesics · Closed geodesics are not constant · Constant curves are not closed geodesics

DefinitionClosed geodesic#✓fully proved

Let \(X\) be a pseudo-extended metric space. A curve \(\gamma : \mathbb{R} \to X\) is a closed geodesic if it is a geodesic defined on all of \(\mathbb{R}\), it is periodic with some period \(T > 0\) (that is, \(\gamma(t + T) = \gamma(t)\) for all \(t \in \mathbb{R}\)), and it is not constant: \(\gamma(t_1) \ne \gamma(t_2)\) for some \(t_1, t_2 \in \mathbb{R}\).

Periodicity of a geodesic defined on all of \(\mathbb{R}\) encodes both \(\gamma(0) = \gamma(T)\) and the matching of the velocities at \(0\) and \(T\). For a closed geodesic of speed \(1\), every period \(T > 0\) is the length of \(\gamma\) traversed over one period; its smallest positive period is the length of the underlying prime closed geodesic.

def IsClosedGeodesic (γ : ℝ → X) : Prop :=
  IsGeodesic γ ∧ (∃ T > 0, Function.Periodic γ T) ∧ ∃ t₁ t₂, γ t₁ ≠ γ t₂

Uses 1 · Used by 2

Statement usesGeodesics defined for all times

Used byClosed geodesics are not constant · Constant curves are not closed geodesics

TheoremConstant curves are geodesics#✓fully proved

Let \(X\) be a pseudo-extended metric space. For every point \(p \in X\), the constant curve \(\mathbb{R} \to X\), \(t \mapsto p\), is a geodesic.

Its speed is \(0\).

theorem isGeodesic_const (p : X) : IsGeodesic (fun _ : ℝ ↦ p)

Uses 2

Statement usesGeodesics defined for all times

Proof usesGeodesics of a given speed on a set of times

TheoremConstant curves are not closed geodesics#✓fully proved

Let \(X\) be a pseudo-extended metric space. For every point \(p \in X\), the constant curve \(\mathbb{R} \to X\), \(t \mapsto p\), is not a closed geodesic.

theorem not_isClosedGeodesic_const (p : X) : ¬ IsClosedGeodesic (fun _ : ℝ ↦ p)

Uses 2

Statement usesClosed geodesic

Proof usesGeodesics defined for all times

TheoremStraight lines are geodesics of constant speed#✓fully proved

Let \(F\) be a real normed space and \(p, v \in F\). For every set of times \(s \subseteq \mathbb{R}\), the straight line \(t \mapsto p + t v\) is a geodesic of speed \(\|v\|\) on \(s\).

theorem isGeodesicOnWithSpeed_lineMap {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    (p v : F) (s : Set ℝ) : IsGeodesicOnWithSpeed (fun t : ℝ ↦ p + t • v) s ‖v‖₊

Uses 1 · Used by 1

Statement usesGeodesics of a given speed on a set of times

Used byStraight lines are geodesics

TheoremStraight lines are geodesics#✓fully proved

Let \(F\) be a real normed space. For all \(p, v \in F\), the straight line \(\mathbb{R} \to F\), \(t \mapsto p + t v\), is a geodesic.

theorem isGeodesic_lineMap {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] (p v : F) :
    IsGeodesic (fun t : ℝ ↦ p + t • v)

Uses 3

Statement usesGeodesics defined for all times

Proof usesGeodesics of a given speed on a set of times · Straight lines are geodesics of constant speed

TheoremClosed geodesics are not constant#✓fully proved

Let \(X\) be a pseudo-extended metric space. If \(\gamma : \mathbb{R} \to X\) is a closed geodesic, then for every \(p \in X\), \(\gamma\) is not the constant curve \(t \mapsto p\).

theorem IsClosedGeodesic.not_const {γ : ℝ → X} (h : IsClosedGeodesic γ) (p : X) :
    γ ≠ fun _ ↦ p

Uses 2

Statement usesClosed geodesic

Proof usesGeodesics defined for all times

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.