Geodesics of a Riemannian manifold

A curve in a Riemannian manifold is a geodesic when its velocity is parallel along it: its covariant acceleration D_t γ', taken for the Levi-Civita connection of the manifold's Riemannian bundle instance, vanishes. This file introduces that predicate, carrying the parameter set on which it is asserted, and identifies it with the classical second-order geodesic ODE in a chart.

The covariant acceleration is CovariantDerivative.accelerationWithin, the along-curve derivative CovariantDerivative.alongCurveWithin of the velocity field.

The predicate is stated within a parameter set s, so that a geodesic segment on a closed interval and an all-time geodesic are the same notion at two values of s; the all-time predicate is the s = Set.univ case. Both the velocity TauCeti.Manifold.curveVelocityWithin and its derivative along the curve are then read within s, and the predicate carries UniqueDiffOn ℝ s — satisfied by the nondegenerate intervals and by Set.univ which the theory uses — because that is the hypothesis under which a derivative within s is determined by the curve. Together with the C² regularity it is the hypothesis under which the equation is read as one between honest derivatives. In particular, TauCeti.Manifold.hasDerivWithinAt_derivWithin_extChartAt_comp_curve witnesses the second derivative occurring in the chart equation.

Reading the curve in the extended chart centred at the current point turns the definition into the second-order equation

u'' + Γ_{γ t} (u', u') = 0,

where u = extChartAt I (γ t) ∘ γ and Γ is the model-space Christoffel map of the Levi-Civita connection. That is TauCeti.Manifold.isGeodesicCurveOn_iff_chart. Chart-reading the curve at its current point, rather than in one fixed chart, is what makes this a statement about the whole parameter set at once. The bridge lemma doing the work, CovariantDerivative.accelerationWithin_eq_zero_iff, holds for an arbitrary connection and lives with the rest of the acceleration API in TauCeti/Geometry/Manifold/VectorBundle/CovariantDerivative/AlongCurve/Acceleration.lean.

Main definitions and results

• TauCeti.Manifold.IsGeodesicCurveOn: the geodesic equation on a parameter set, and TauCeti.Manifold.IsGeodesicCurve its all-time case, related by TauCeti.Manifold.isGeodesicCurveOn_univ and unfolded by TauCeti.Manifold.isGeodesicCurve_iff.
• TauCeti.Manifold.IsGeodesicCurveOnFrom: a geodesic together with its initial data, the point and velocity at parameter 0, read off by TauCeti.Manifold.IsGeodesicCurveOnFrom.base_eq and TauCeti.Manifold.IsGeodesicCurveOnFrom.velocity_eq, with TauCeti.Manifold.IsGeodesicCurveOnFrom.hasMFDerivAt_zero the unrestricted derivative at 0.
• TauCeti.Manifold.isGeodesicCurveOn_iff_chart: the geodesic equation in a chart, the second-order ODE u'' + Γ (u', u') = 0.
• TauCeti.Manifold.hasDerivWithinAt_derivWithin_extChartAt_comp_curve: the second within-derivative in that ODE is the derivative of the first one, rather than a junk value.
• TauCeti.Manifold.isGeodesicCurveOn_iff_of_isOpen: on an open parameter set the equation is the unrestricted one.
• TauCeti.Manifold.isGeodesicCurveOn_const: a constant curve is a geodesic.
• TauCeti.Manifold.IsGeodesicCurveOn.alongCurveWithin_smul_curveVelocityWithin: the covariant derivative of f γ' along a geodesic is f' γ'.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 3, §2.
• J. M. Lee, Introduction to Riemannian Manifolds, GTM 176, 2018, Ch. 4.

The geodesic equation

structure TauCeti.Manifold.IsGeodesicCurveOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (γ : ℝ → M) (s : Set ℝ) : Prop

A geodesic on a parameter set: a C² curve whose covariant acceleration within s, taken for the Levi-Civita connection of the ambient Riemannian bundle instance, vanishes.

The covariant acceleration is CovariantDerivative.accelerationWithin, the derivative along the curve of the velocity TauCeti.Manifold.curveVelocityWithin, both taken within s.

• uniqueDiffOn : UniqueDiffOn ℝ s

  The parameter set has unique derivatives. Without this the derivatives within s are not determined by the curve, and the geodesic equation below does not say what it should.

• contMDiffOn : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 2 γ s

  A geodesic is C² on its parameter set, so the two derivatives in its chart equation are genuine within-derivatives.

• accelerationWithin_eq_zero (r : ℝ) : r ∈ s → (CovariantDerivative.leviCivitaConnection I M).accelerationWithin γ s r = 0

  The geodesic equation: the covariant acceleration vanishes at every parameter of s.

def TauCeti.Manifold.IsGeodesicCurve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (γ : ℝ → M) : Prop

A geodesic, defined at every real parameter. This is the s = Set.univ case of TauCeti.Manifold.IsGeodesicCurveOn.

theorem TauCeti.Manifold.isGeodesicCurveOn_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} : IsGeodesicCurveOn I γ Set.univ ↔ IsGeodesicCurve I γ

Asserting the geodesic equation on the whole parameter space gives the all-time predicate.

theorem TauCeti.Manifold.IsGeodesicCurveOn.mdifferentiableOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} (h : IsGeodesicCurveOn I γ s) : MDiff[s] γ

A geodesic is differentiable on its parameter set.

theorem TauCeti.Manifold.IsGeodesicCurveOn.continuousOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} (h : IsGeodesicCurveOn I γ s) : ContinuousOn γ s

A geodesic is continuous on its parameter set.

structure TauCeti.Manifold.IsGeodesicCurveOnFrom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (γ : ℝ → M) (s : Set ℝ) (p : M) (v : TangentSpace I p) : Prop

A geodesic with prescribed initial data: a geodesic on a parameter set containing 0 which starts at p with velocity v. The two pieces of initial data are packaged as a single equality of points of the tangent bundle, which avoids transporting v along γ 0 = p and is the form in which the geodesic flow on TM will consume them.

• isGeodesicCurveOn : IsGeodesicCurveOn I γ s

  The curve is a geodesic on s.

• zero_mem : 0 ∈ s

  The initial parameter belongs to the parameter set.

• initial_eq : ⟨γ 0, curveVelocityWithin I γ s 0⟩ = ⟨p, v⟩

  The curve leaves p with velocity v.

theorem TauCeti.Manifold.IsGeodesicCurveOnFrom.base_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} {p : M} {v : TangentSpace I p} (h : IsGeodesicCurveOnFrom I γ s p v) : γ 0 = p

A geodesic with initial data starts at the prescribed point.

theorem TauCeti.Manifold.IsGeodesicCurveOnFrom.velocity_heq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} {p : M} {v : TangentSpace I p} (h : IsGeodesicCurveOnFrom I γ s p v) : curveVelocityWithin I γ s 0 ≍ v

A geodesic with initial data leaves with the prescribed velocity. The equality is heterogeneous because the two sides live in the tangent spaces at γ 0 and at p.

theorem TauCeti.Manifold.IsGeodesicCurveOnFrom.velocity_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} {p : M} {v : TangentSpace I p} (h : IsGeodesicCurveOnFrom I γ s p v) : cast ⋯ (curveVelocityWithin I γ s 0) = v

A geodesic with initial data leaves with the prescribed velocity, transported to TangentSpace I p along TauCeti.Manifold.IsGeodesicCurveOnFrom.base_eq.

theorem TauCeti.Manifold.IsGeodesicCurveOnFrom.hasMFDerivAt_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} {p : M} {v : TangentSpace I p} (h : IsGeodesicCurveOnFrom I γ s p v) (hs : s ∈ nhds 0) : HasMFDerivAt% γ 0 (ContinuousLinearMap.smulRight 1 v)

A geodesic with initial data (p, v) on a neighbourhood of 0 has v as its unrestricted velocity at 0.

theorem TauCeti.Manifold.IsGeodesicCurveOn.isGeodesicCurveOnFrom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} (h : IsGeodesicCurveOn I γ s) (h0 : 0 ∈ s) : IsGeodesicCurveOnFrom I γ s (γ 0) (curveVelocityWithin I γ s 0)

A geodesic on a parameter set containing 0 is a geodesic with the initial data it has there.

The geodesic equation in a chart

theorem TauCeti.Manifold.isGeodesicCurveOn_iff_chart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} (hs : UniqueDiffOn ℝ s) : IsGeodesicCurveOn I γ s ↔ ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 2 γ s ∧ ∀ r ∈ s, derivWithin (derivWithin (↑(extChartAt I (γ r)) ∘ γ) s) s r + ((christoffelMap (Module.finBasis ℝ E) ⋯ (γ r)) (derivWithin (↑(extChartAt I (γ r)) ∘ γ) s r)) (derivWithin (↑(extChartAt I (γ r)) ∘ γ) s r) = 0

The geodesic equation in a chart. A C² curve is a geodesic on a parameter set with unique derivatives exactly when, at every parameter of that set, the curve read in the extended chart centred at the current point solves u'' + Γ (u', u') = 0, with Γ the model-space Christoffel map of the Levi-Civita connection in the tangent-bundle trivialization there.

theorem TauCeti.Manifold.IsGeodesicCurveOn.congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} {γ' : ℝ → M} (h : IsGeodesicCurveOn I γ s) (hγ : Set.EqOn γ' γ s) : IsGeodesicCurveOn I γ' s

Being a geodesic on a parameter set depends only on the values of the curve on that set.

Open parameter sets

theorem TauCeti.Manifold.isGeodesicCurveOn_iff_of_isOpen {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} (hs : IsOpen s) : IsGeodesicCurveOn I γ s ↔ ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 2 γ s ∧ ∀ r ∈ s, (CovariantDerivative.leviCivitaConnection I M).acceleration γ r = 0

On an open parameter set, the geodesic equation is the unrestricted one.

theorem TauCeti.Manifold.isGeodesicCurve_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} : IsGeodesicCurve I γ ↔ ContMDiff (modelWithCornersSelf ℝ ℝ) I 2 γ ∧ ∀ (t : ℝ), (CovariantDerivative.leviCivitaConnection I M).acceleration γ t = 0

The all-time geodesic equation, spelled out.

Constant curves

theorem TauCeti.Manifold.isGeodesicCurveOn_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {s : Set ℝ} (hs : UniqueDiffOn ℝ s) (x : M) : IsGeodesicCurveOn I (fun (x_1 : ℝ) => x) s

A constant curve is a geodesic. Its covariant acceleration vanishes.

theorem TauCeti.Manifold.isGeodesicCurve_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (x : M) : IsGeodesicCurve I fun (x_1 : ℝ) => x

A constant curve is an all-time geodesic.

Scalar multiples of the velocity

theorem TauCeti.Manifold.IsGeodesicCurveOn.alongCurveWithin_smul_curveVelocityWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} {t : ℝ} (h : IsGeodesicCurveOn I γ s) {f : ℝ → ℝ} (ht : t ∈ s) (hf : DifferentiableWithinAt ℝ f s t) : (CovariantDerivative.leviCivitaConnection I M).alongCurveWithin γ (fun (r : ℝ) => f r • curveVelocityWithin I γ s r) s t = derivWithin f s t • curveVelocityWithin I γ s t

The covariant derivative of a scalar multiple of the velocity of a geodesic is the derivative of the scalar times the velocity, since the velocity field of a geodesic is parallel.