Geodesic flow

DefinitionUnit tangent bundle of a Riemannian manifold#✓fully proved

The unit tangent bundle SM of a Riemannian manifold (M, g): the tangent vectors whose norm for the installed metric on their fiber is 1, as a set of TangentBundle I M with the subspace topology. Source: Burns-Matveev, ETDS 41 (2021), §1 ("the unit tangent bundle ... is denoted by SM").

def unitTangentBundle (I : ModelWithCorners ℝ E H) (M : Type*) [TopologicalSpace M]
    [ChartedSpace H M] [RiemannianBundle (fun x : M ↦ TangentSpace I x)] :
    Set (TangentBundle I M) :=
  {p : TangentBundle I M | ‖p.snd‖ = 1}

Used by 2

Used byGeodesic flow on the unit tangent bundle · The unit geodesic flow of Euclidean space is the straight-line flow

StructureGeodesic velocity curves#✓fully proved

Let \(M\) be a \(C^2\) manifold (boundary and corners allowed) modeled on a finite-dimensional real space, with a \(C^1\) Riemannian metric \(\langle \cdot, \cdot \rangle\) and Levi-Civita connection \(\nabla\). A curve \(u : \mathbb{R} \to TM\), with base curve \(\gamma\) (\(\gamma(t)\) is the base point of \(u(t)\)), is a geodesic velocity curve when for every \(t \in \mathbb{R}\): \(\gamma\) is differentiable at \(t\) with velocity \(\gamma'(t) = u(t)\); and for every vector field \(W\) on \(M\) that is differentiable at \(\gamma(t)\), the function \(s \mapsto \langle u(s), W(\gamma(s)) \rangle\) has derivative \(\langle u(t), \nabla_{u(t)} W \rangle\) at \(t\).

The second condition is the weak form of the geodesic equation \(\nabla_{\gamma'} \gamma' = 0\): by metric compatibility, \(\frac{d}{dt} \langle \gamma', W \circ \gamma \rangle = \langle \nabla_{\gamma'} \gamma', W \rangle + \langle \gamma', \nabla_{\gamma'} W \rangle\), and the values \(W(\gamma(t))\) exhaust the tangent space. The two conditions force \(\gamma\) to be \(C^2\) in charts, where the weak form is equivalent to \(\nabla_{\gamma'} \gamma' = 0\); no further smoothness of the curve is assumed.

Manifold.IsGeodesicVelocityCurve · 18 lines

structure IsGeodesicVelocityCurve (I : ModelWithCorners ℝ E H) {M : Type*}
    [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M]
    [RiemannianBundle (fun x : M ↦ TangentSpace I x)]
    [IsContMDiffRiemannianBundle I 1 E (fun x : M ↦ TangentSpace I x)]
    [FiniteDimensional ℝ E] (u : ℝ → TangentBundle I M) : Prop where
  /-- Velocity link: the base curve `fun s ↦ (u s).proj` has manifold derivative at `t`
  equal to `ContinuousLinearMap.toSpanSingleton ℝ (u t).snd`, i.e. its velocity at `t` is the
  fiber component of `u t`. -/
  hasMFDerivAt_proj : ∀ (t : ℝ), HasMFDerivAt 𝓘(ℝ, ℝ) I (fun s ↦ (u s).proj) t
    (ContinuousLinearMap.toSpanSingleton ℝ (u t).snd)
  /-- Geodesic equation, weak form: for every vector field `W` differentiable at the base point,
  the real function `s ↦ ⟪(u s).snd, W (u s).proj⟫` has derivative at `t` equal to
  `⟪(u t).snd, ∇_{(u t).snd} W⟫`, with `∇ = CovariantDerivative.leviCivitaConnection I M`. -/
  hasDerivAt_inner : ∀ (t : ℝ) (W : Π x : M, TangentSpace I x),
    MDiffAt (T% W) (u t).proj →
      HasDerivAt (fun s ↦ inner ℝ (u s).snd (W (u s).proj))
        (inner ℝ (u t).snd
          (CovariantDerivative.leviCivitaConnection I M W (u t).proj (u t).snd)) t

Used by 5

Used byGeodesic flow on the tangent bundle · The geodesic flow of Euclidean space is the straight-line flow · Geodesic velocity curves in Euclidean space · Geodesic flow on the unit tangent bundle · The unit geodesic flow of Euclidean space is the straight-line flow

StructureGeodesic flow on the tangent bundle#✓fully proved

Let \(M\) be a \(C^2\) manifold (boundary and corners allowed) modeled on a finite-dimensional real space, with a \(C^1\) Riemannian metric \(g\). A family of maps \(\varphi_t : TM \to TM\), \(t \in \mathbb{R}\), is a geodesic flow of \(g\) when \(\varphi_0(v) = v\) for every \(v \in TM\), \(\varphi_{t+s}(v) = \varphi_t(\varphi_s(v))\) for all \(t, s \in \mathbb{R}\) and \(v \in TM\), and for every \(v \in TM\) the orbit \(t \mapsto \varphi_t(v)\) is a geodesic velocity curve. Then \(\varphi_t(v) = \gamma_v'(t)\) for a geodesic \(\gamma_v\) with initial velocity \(v\).

The definition characterizes the flow and does not assert that one exists or is unique. For a \(C^\infty\) metric on a boundaryless manifold, uniqueness is classical, and the global flow exists when the metric is also complete. No continuity, smoothness or conservation of speed is assumed.

structure IsGeodesicFlow (I : ModelWithCorners ℝ E H) {M : Type*}
    [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M]
    [RiemannianBundle (fun x : M ↦ TangentSpace I x)]
    [IsContMDiffRiemannianBundle I 1 E (fun x : M ↦ TangentSpace I x)]
    [FiniteDimensional ℝ E] (φ : ℝ → TangentBundle I M → TangentBundle I M) : Prop where
  /-- The flow at time `0` is the identity: `φ 0 v = v` for every `v`. -/
  map_zero : ∀ (v : TangentBundle I M), φ 0 v = v
  /-- Flow law: `φ (t + s) v = φ t (φ s v)` for all times `t s` and every `v`. -/
  map_add : ∀ (t s : ℝ) (v : TangentBundle I M), φ (t + s) v = φ t (φ s v)
  /-- Every orbit `fun t ↦ φ t v` is a geodesic velocity curve. -/
  isGeodesicVelocityCurve : ∀ (v : TangentBundle I M),
    IsGeodesicVelocityCurve I (fun t ↦ φ t v)

Uses 1 · Used by 1

Statement usesGeodesic velocity curves

Used byThe geodesic flow of Euclidean space is the straight-line flow

StructureGeodesic flow on the unit tangent bundle#✓fully proved

Let \(M\) be a \(C^2\) manifold (boundary and corners allowed) modeled on a finite-dimensional real space, with a \(C^1\) Riemannian metric \(g\) and unit tangent bundle \(SM\). A family of maps \(\varphi_t : SM \to SM\), \(t \in \mathbb{R}\), is a geodesic flow on \(SM\) when \(\varphi_0(v) = v\) for every \(v \in SM\), \(\varphi_{t+s}(v) = \varphi_t(\varphi_s(v))\) for all \(t, s \in \mathbb{R}\) and \(v \in SM\), and for every \(v \in SM\) the orbit \(t \mapsto \varphi_t(v)\), viewed as a curve in \(TM\), is a geodesic velocity curve. This is the geodesic flow \(\varphi_t\) on \(SM\) of Burns–Matveev §1: the orbit of \(v\) is the velocity curve of a unit-speed geodesic \(\gamma_v\) with initial velocity \(v\).

The definition characterizes the flow and does not assert that one exists or is unique. For a \(C^\infty\) metric on a boundaryless manifold, uniqueness is classical, and the global flow exists when the metric is also complete. No continuity, smoothness or conservation of speed is assumed.

structure IsUnitGeodesicFlow (I : ModelWithCorners ℝ E H) {M : Type*}
    [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M]
    [RiemannianBundle (fun x : M ↦ TangentSpace I x)]
    [IsContMDiffRiemannianBundle I 1 E (fun x : M ↦ TangentSpace I x)]
    [FiniteDimensional ℝ E]
    (φ : ℝ → unitTangentBundle I M → unitTangentBundle I M) : Prop where
  /-- The flow at time `0` is the identity: `φ 0 v = v` for every `v`. -/
  map_zero : ∀ (v : unitTangentBundle I M), φ 0 v = v
  /-- Flow law: `φ (t + s) v = φ t (φ s v)` for all times `t s` and every `v`. -/
  map_add : ∀ (t s : ℝ) (v : unitTangentBundle I M), φ (t + s) v = φ t (φ s v)
  /-- Every orbit `fun t ↦ (φ t v : TangentBundle I M)` is a geodesic velocity curve. -/
  isGeodesicVelocityCurve : ∀ (v : unitTangentBundle I M),
    IsGeodesicVelocityCurve I (fun t ↦ (φ t v : TangentBundle I M))

Uses 2 · Used by 1

Statement usesGeodesic velocity curves · Unit tangent bundle of a Riemannian manifold

Used byThe unit geodesic flow of Euclidean space is the straight-line flow

TheoremGeodesic velocity curves in Euclidean space#✓fully proved

Let \(F\) be a finite-dimensional real inner product space, viewed as a Riemannian manifold with the metric given by its inner product, and identify each tangent space of \(F\) with \(F\), so that a point of the tangent bundle \(TF\) is a pair \((x, v)\) with \(x, v \in F\). A curve \(t \mapsto u(t) = (x(t), v(t))\) in \(TF\), defined for all real \(t\), is the velocity curve of a geodesic if and only if, for every real \(t\), \(x(t) = x(0) + t\,v(0)\) and \(v(t) = v(0)\).

theorem isGeodesicVelocityCurve_vectorSpace_iff
    (u : ℝ → TangentBundle 𝓘(ℝ, F) F) :
    IsGeodesicVelocityCurve 𝓘(ℝ, F) u ↔ ∀ t,
      (u t).proj = (u 0).proj +
        t • NormedSpace.fromTangentSpace ((u 0).proj) ((u 0).snd) ∧
      NormedSpace.fromTangentSpace ((u t).proj) ((u t).snd) =
        NormedSpace.fromTangentSpace ((u 0).proj) ((u 0).snd)

Uses 5 · Used by 2

Statement usesGeodesic velocity curves

Proof usesThe Levi-Civita connection of Euclidean space kills constant vector fields · The Levi-Civita connection of a vector space is the Fréchet derivative · Extending a tangent vector of a normed space gives a constant vector field · Extensions of tangent vectors of a normed space are differentiable

Used byThe geodesic flow of Euclidean space is the straight-line flow · The unit geodesic flow of Euclidean space is the straight-line flow

TheoremThe geodesic flow of Euclidean space is the straight-line flow#✓fully proved

Let \(F\) be a finite-dimensional real inner product space, viewed as a Riemannian manifold with the metric given by its inner product, and identify each tangent space of \(F\) with \(F\), so that a point of the tangent bundle \(TF\) is a pair \((x, v)\) with \(x, v \in F\). A family of maps \(\varphi_t \colon TF \to TF\), \(t \in \mathbb{R}\), is a geodesic flow on \(TF\) if and only if \(\varphi_t(x, v) = (x + t v, v)\) for every real \(t\) and every \((x, v) \in TF\).

theorem isGeodesicFlow_vectorSpace_iff
    (φ : ℝ → TangentBundle 𝓘(ℝ, F) F → TangentBundle 𝓘(ℝ, F) F) :
    IsGeodesicFlow 𝓘(ℝ, F) φ ↔ ∀ t p,
      (φ t p).proj = p.proj +
        t • NormedSpace.fromTangentSpace (p.proj) (p.snd) ∧
      NormedSpace.fromTangentSpace ((φ t p).proj) ((φ t p).snd) =
        NormedSpace.fromTangentSpace (p.proj) (p.snd)

Uses 3

Statement usesGeodesic flow on the tangent bundle

Proof usesGeodesic velocity curves · Geodesic velocity curves in Euclidean space

TheoremThe unit geodesic flow of Euclidean space is the straight-line flow#✓fully proved

Let \(F\) be a finite-dimensional real inner product space, viewed as a Riemannian manifold with the metric given by its inner product, and identify each tangent space of \(F\) with \(F\), so that a point of the tangent bundle is a pair \((x, v)\) with \(x, v \in F\), and the unit tangent bundle \(SF\) consists of the pairs with \(\|v\| = 1\). A family of maps \(\varphi_t \colon SF \to SF\), \(t \in \mathbb{R}\), is a geodesic flow on \(SF\) if and only if \(\varphi_t(x, v) = (x + t v, v)\) for every real \(t\) and every \((x, v) \in SF\).

Manifold.isUnitGeodesicFlow_vectorSpace_iff · 15 lines

theorem isUnitGeodesicFlow_vectorSpace_iff
    (φ : ℝ → unitTangentBundle 𝓘(ℝ, F) F →
      unitTangentBundle 𝓘(ℝ, F) F) :
    IsUnitGeodesicFlow 𝓘(ℝ, F) φ ↔ ∀ t p,
      (↑(φ t p) : TangentBundle 𝓘(ℝ, F) F).proj =
        (↑p : TangentBundle 𝓘(ℝ, F) F).proj +
          t • NormedSpace.fromTangentSpace
            (↑p : TangentBundle 𝓘(ℝ, F) F).proj
            (↑p : TangentBundle 𝓘(ℝ, F) F).snd ∧
      NormedSpace.fromTangentSpace
          (↑(φ t p) : TangentBundle 𝓘(ℝ, F) F).proj
          (↑(φ t p) : TangentBundle 𝓘(ℝ, F) F).snd =
        NormedSpace.fromTangentSpace
          (↑p : TangentBundle 𝓘(ℝ, F) F).proj
          (↑p : TangentBundle 𝓘(ℝ, F) F).snd

Uses 4

Statement usesGeodesic flow on the unit tangent bundle · Unit tangent bundle of a Riemannian manifold

Proof usesGeodesic velocity curves · Geodesic velocity curves in Euclidean space

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.