The geodesic spray

The geodesic equation u'' + Γ (u', u') = 0 is a second-order equation on the manifold; as usual it becomes a first-order equation on the tangent bundle, for the vector field

S (x, v) = (v, -Γ_x (v, v))

on TM called the geodesic spray. This file constructs S for the Levi-Civita connection of the ambient Riemannian bundle instance, identifies velocity lifts of C² geodesics with integral curves of S, and shows that every integral curve is a velocity lift.

A vector field on a manifold assigns to a point a vector of the model space, read in the chart at that point; the tangent-bundle chart at z = (x, v) reads the base direction in the extended chart of M at x and the fibre direction in the tangent-bundle trivialization at x, over which v is its own coordinate. So the displayed formula is the definition of TauCeti.Manifold.geodesicSpray, with Γ the model-space Christoffel map TauCeti.Manifold.christoffelMap of the Levi-Civita connection in the trivialization at the base point of the argument — the same moving-chart convention as CovariantDerivative.alongCurveWithin and TauCeti.Manifold.IsGeodesicCurveOn. Its compatibility on overlapping tangent-bundle charts is TauCeti.Manifold.tangentCoordChange_geodesicSpray; the derivative term in the tangent lift cancels the inhomogeneous term in TauCeti.Manifold.christoffelMap_coordChange. That this formula solves the intended problem is the content of TauCeti.Manifold.isMIntegralCurveOn_curveVelocityLiftWithin_iff and TauCeti.Manifold.eq_curveVelocityLiftWithin_of_isMIntegralCurveOn: on a parameter set with unique derivatives, velocity lifts of C² geodesics are integral curves of S, while arbitrary integral curves of S are velocity lifts of their projected curves:

t ↦ (γ t, γ' t) : ℝ → TM

The two statements are read in one direction each: the velocity lift of a C² curve is an integral curve of S exactly when the curve is a geodesic, and conversely every integral curve of S is the velocity lift of the curve it lies over, whose base curve is a geodesic as soon as it is C². The C² hypothesis on the base curve is not yet removable: it would follow from smoothness of S, which is not proved here.

The unpacking of a curve into TM into its base curve and its fibre coordinate is TauCeti.Manifold.hasMFDerivWithinAt_totalSpace_curve_iff, proved for an arbitrary fibre bundle.

Main definitions and results

• TauCeti.Manifold.geodesicSpray: the geodesic spray of the ambient Riemannian bundle instance, a vector field on the tangent bundle, with TauCeti.Manifold.geodesicSpray_apply its preferred-chart formula and TauCeti.Manifold.tangentCoordChange_geodesicSpray its formula in every overlapping tangent-bundle chart.
• TauCeti.Manifold.hasMFDerivWithinAt_curveVelocityLiftWithin_iff: at one parameter, the velocity lift of a C² curve solves the spray equation exactly when the covariant derivative of the velocity along the curve vanishes.
• TauCeti.Manifold.isMIntegralCurveOn_curveVelocityLiftWithin_iff: the velocity lift of a C² curve is an integral curve of the geodesic spray exactly when the curve is a geodesic, with TauCeti.Manifold.isMIntegralCurve_curveVelocityLift_iff its all-time case.
• TauCeti.Manifold.eq_curveVelocityLiftWithin_of_isMIntegralCurveOn: an integral curve of the geodesic spray is a velocity lift, and TauCeti.Manifold.isGeodesicCurveOn_proj_of_isMIntegralCurveOn: the curve it lies over is a geodesic once it is C².

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 spray

noncomputable def TauCeti.Manifold.geodesicSpray {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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] (z : TangentBundle I M) : TangentSpace I.tangent z

The geodesic spray of the ambient Riemannian bundle instance: the vector field (x, v) ↦ (v, -Γ_x (v, v)) on the tangent bundle, where Γ is the model-space Christoffel map of the Levi-Civita connection in the tangent-bundle trivialization at x. Both components are read in the tangent-bundle chart centred at the argument, in which the base direction is read in the extended chart of M at x and the fibre direction in the trivialization at x.

Equations

• TauCeti.Manifold.geodesicSpray I M z = (z.snd, -((TauCeti.Manifold.christoffelMap (Module.finBasis ℝ E) ⋯ z.proj) z.snd) z.snd)

theorem TauCeti.Manifold.geodesicSpray_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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] (z : TangentBundle I M) : geodesicSpray I M z = (z.snd, -((christoffelMap (Module.finBasis ℝ E) ⋯ z.proj) z.snd) z.snd)

The chart formula for the geodesic spray, restating the definition, whose body is not exposed across the module boundary.

@[simp]

theorem TauCeti.Manifold.geodesicSpray_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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) : geodesicSpray I M ⟨x, 0⟩ = 0

The geodesic spray vanishes on the zero section of the tangent bundle.

theorem TauCeti.Manifold.tangentCoordChange_geodesicSpray {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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 x₀ : M} (hx₀ : x ∈ (extChartAt I x₀).source) (u : TangentSpace I x) : (tangentCoordChange I.tangent ⟨x, u⟩ ⟨x₀, 0⟩ ⟨x, u⟩) (geodesicSpray I M ⟨x, u⟩) = have v := (tangentCoordChange I x x₀ x) u; (v, -((christoffelMap (Module.finBasis ℝ E) ⋯ x) v) v)

The geodesic spray has the same formula in every overlapping tangent-bundle chart. Transporting the value defined in the preferred chart at (x, u) to the chart based at x₀ sends (v, -Γ(v, v)) to (v₀, -Γ₀(v₀, v₀)), where v₀ is the fibre coordinate in the latter chart.

theorem TauCeti.Manifold.hasMFDerivWithinAt_curveVelocityLiftWithin_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {γ : ℝ → M} {s : Set ℝ} {t : ℝ} [FiniteDimensional ℝ E] [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] (hs : UniqueDiffOn ℝ s) (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 2 γ s) (ht : t ∈ s) : HasMFDerivAt[s] (curveVelocityLiftWithin I γ s) t (ContinuousLinearMap.smulRight 1 (geodesicSpray I M (curveVelocityLiftWithin I γ s t))) ↔ (CovariantDerivative.leviCivita I M).alongCurveWithin γ (curveVelocityWithin I γ s) s t = 0

The geodesic equation as an integral-curve equation. The velocity lift of a C² curve solves the equation of the geodesic spray at a parameter of its set exactly when the derivative of its velocity along it vanishes there.

theorem TauCeti.Manifold.isMIntegralCurveOn_curveVelocityLiftWithin_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {γ : ℝ → M} {s : Set ℝ} [FiniteDimensional ℝ E] [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] (hs : UniqueDiffOn ℝ s) (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 2 γ s) : IsMIntegralCurveOn (curveVelocityLiftWithin I γ s) (geodesicSpray I M) s ↔ IsGeodesicCurveOn I γ s

Geodesics are the base curves of the spray. The velocity lift of a C² curve is an integral curve of the geodesic spray on a parameter set with unique derivatives exactly when the curve is a geodesic there.

theorem TauCeti.Manifold.eq_curveVelocityLiftWithin_of_isMIntegralCurveOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {s : Set ℝ} {t : ℝ} [FiniteDimensional ℝ E] [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] {z : ℝ → TangentBundle I M} (hs : UniqueDiffWithinAt ℝ s t) (h : IsMIntegralCurveOn z (geodesicSpray I M) s) (ht : t ∈ s) : z t = curveVelocityLiftWithin I (fun (r : ℝ) => (z r).proj) s t

An integral curve of the spray is a velocity lift. At a parameter at which the parameter set has unique derivatives, an integral curve of the geodesic spray is the velocity lift of the curve it lies over.

theorem TauCeti.Manifold.isGeodesicCurveOn_proj_of_isMIntegralCurveOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {s : Set ℝ} [FiniteDimensional ℝ E] [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] {z : ℝ → TangentBundle I M} (hs : UniqueDiffOn ℝ s) (h : IsMIntegralCurveOn z (geodesicSpray I M) s) (hz : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 2 (fun (r : ℝ) => (z r).proj) s) : IsGeodesicCurveOn I (fun (r : ℝ) => (z r).proj) s

The base curve of an integral curve of the spray is a geodesic, as soon as it is C² on a parameter set with unique derivatives.

All-time geodesics and the spray

theorem TauCeti.Manifold.isMIntegralCurve_curveVelocityLift_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {γ : ℝ → M} [FiniteDimensional ℝ E] [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] (hγ : ContMDiff (modelWithCornersSelf ℝ ℝ) I 2 γ) : IsMIntegralCurve (curveVelocityLift I γ) (geodesicSpray I M) ↔ IsGeodesicCurve I γ

The all-time case of TauCeti.Manifold.isMIntegralCurveOn_curveVelocityLiftWithin_iff: the velocity lift of a C² curve is an integral curve of the geodesic spray exactly when the curve is an all-time geodesic.