Geodesics of a Riemannian manifold

A curve in a Riemannian manifold is a geodesic when its velocity is parallel along it: the derivative of the velocity field along the curve, 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 derivative along the curve is the moving-chart candidate CovariantDerivative.alongCurveWithin. That candidate is identified with the ambient covariant derivative for fields pulled back from an ambient vector field, by CovariantDerivative.alongCurveWithin_pullback; the velocity field of a curve is not such a pullback, so for it the identification — and with it the chart independence of the predicate — remains open, exactly as the definition of the operator records.

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 the along-curve derivative CovariantDerivative.alongCurveWithin 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 intended to be read as one between honest derivatives; that the two of them do make the chart reading of the curve twice differentiable within s is not yet formalized, so the derivWithins below may still carry the junk value 0.

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 lemmas doing the work, TauCeti.Manifold.sectionCoord_curveVelocityWithin_eventuallyEq and CovariantDerivative.alongCurveWithin_curveVelocityWithin_eq_zero_iff, hold for an arbitrary connection and live with the rest of the along-curve API in TauCeti/Geometry/Manifold/VectorBundle/CovariantDerivative/AlongCurve/Pullback.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.
• TauCeti.Manifold.isGeodesicCurveOn_iff_chart: the geodesic equation in a chart, the second-order ODE u'' + Γ (u', u') = 0.
• 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.

References

• Geodesics, the exponential map, and the Hopf--Rinow theorem roadmap, Layer 1, "IsGeodesicCurveOn γ s" and "Initial data".
• 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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [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 velocity within s is annihilated by the moving-chart candidate for the derivative along the curve, taken for the Levi-Civita connection of the ambient Riemannian bundle instance.

The velocity is TauCeti.Manifold.curveVelocityWithin and the candidate for its derivative along the curve is CovariantDerivative.alongCurveWithin, both taken within s. The candidate is identified with the ambient covariant derivative only for pulled-back fields, which the velocity field is not.

• 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: this is the regularity under which the geodesic equation is intended to be an equation between honest derivatives. That it does make the chart reading of the curve twice differentiable within s is not yet formalized, so the equation may still read the junk values of CovariantDerivative.alongCurveInChartWithin.

• alongCurveWithin_curveVelocityWithin_eq_zero (r : ℝ) : r ∈ s → (CovariantDerivative.leviCivita I M).alongCurveWithin γ (curveVelocityWithin I γ s) s r = 0

  The geodesic equation: the along-curve candidate annihilates the velocity field 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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [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.

Equations

• TauCeti.Manifold.IsGeodesicCurve I γ = TauCeti.Manifold.IsGeodesicCurveOn I γ Set.univ

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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [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.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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [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.

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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [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.leviCivita I M).alongCurve γ (curveVelocity I γ) 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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [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.leviCivita I M).alongCurve γ (curveVelocity I γ) 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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [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 velocity field is the zero section, which the along-curve candidate annihilates.

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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [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.