Smoothness of the geodesic spray and of geodesics

The geodesic spray of a smooth Riemannian manifold is a smooth vector field on its tangent bundle. In tangent-bundle coordinates it is

(x, v) ↦ (v, -Γₓ(v, v)),

so this follows from smoothness of the Christoffel map of the Levi-Civita connection. This is the regularity input needed to apply existence and uniqueness theorems for integral curves to the geodesic equation.

A geodesic TauCeti.Manifold.IsGeodesicCurveOn is only required to be C². Its velocity lift is an integral curve of the spray, so it gains one derivative over the spray, and the curve gains one derivative over its velocity lift. Bootstrapping, a geodesic of a C^(n + 1) metric on a C^(n + 2) manifold is C^(n + 2), and a geodesic of a smooth metric is smooth. These hold on any parameter set with unique derivatives, including a nondegenerate closed interval up to its endpoints, so no extension of the geodesic beyond its interval is needed.

Main result

• TauCeti.Manifold.contMDiff_geodesicSpray: the geodesic spray is C^n when the manifold is C^(n + 2) and its Riemannian metric is C^(n + 1), with TauCeti.Manifold.contMDiff_one_geodesicSpray the C^1 case consumed by the integral-curve API and TauCeti.Manifold.contMDiff_infty_geodesicSpray the smooth case used for geodesic flows.
• TauCeti.Manifold.isGeodesicCurveOn_proj_of_isMIntegralCurveOn: every spray integral curve on a set with unique derivatives projects to a geodesic.
• IsMIntegralCurveOn.isGeodesicCurveOnFrom_proj: its initial data are encoded by its value at zero, including for nondegenerate closed parameter intervals.
• TauCeti.Manifold.IsGeodesicCurveOn.contMDiffOn_of_le: a geodesic of a C^(n + 1) metric on a C^(n + 2) manifold is C^(n + 2) on its parameter set, with TauCeti.Manifold.IsGeodesicCurveOn.contMDiffOn_curveVelocityLiftWithin_of_le the C^(n + 1) regularity of its velocity lift.
• TauCeti.Manifold.IsGeodesicCurveOn.contMDiffOn_infty: geodesics of a smooth metric are smooth, with the pointwise form TauCeti.Manifold.IsGeodesicCurveOn.contMDiffAt_infty at interior parameters, the all-time form TauCeti.Manifold.IsGeodesicCurve.contMDiff_infty and the velocity-lift form TauCeti.Manifold.IsGeodesicCurveOn.contMDiffOn_curveVelocityLiftWithin_infty.

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.

theorem TauCeti.Manifold.contMDiff_geodesicSpray {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {n m k : WithTop ℕ∞} [IsManifold I 2 M] [IsManifold I m M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I k E fun (x : M) => TangentSpace I x] (hm : n + 2 ≤ m) (hk : n + 1 ≤ k) : ContMDiff I.tangent I.tangent.tangent n fun (z : TangentBundle I M) => ⟨z, geodesicSpray I M z⟩

The geodesic spray is a C^n vector field on the tangent bundle. A C^(n + 1) metric and C^(n + 2) manifold structure suffice. In particular, the spray of a smooth Riemannian manifold is smooth.

theorem TauCeti.Manifold.contMDiff_one_geodesicSpray {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 3 M] [IsContMDiffRiemannianBundle I 2 E fun (x : M) => TangentSpace I x] : ContMDiff I.tangent I.tangent.tangent 1 fun (z : TangentBundle I M) => ⟨z, geodesicSpray I M z⟩

The geodesic spray is a C^1 vector field on the tangent bundle of a C^3 manifold with a C^2 Riemannian metric. This is the regularity at which Mathlib's integral-curve existence, uniqueness and extension theorems consume the spray.

theorem TauCeti.Manifold.contMDiff_infty_geodesicSpray {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] : ContMDiff I.tangent I.tangent.tangent ↑⊤ fun (z : TangentBundle I M) => ⟨z, geodesicSpray I M z⟩

The geodesic spray is a smooth vector field on the tangent bundle of a smooth manifold with a smooth Riemannian metric.

theorem TauCeti.Manifold.isGeodesicCurveOn_proj_of_isMIntegralCurveOn {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [I.Boundaryless] [IsManifold I 3 M] [IsContMDiffRiemannianBundle I 2 E fun (x : M) => TangentSpace I x] {z : ℝ → TangentBundle I M} {s : Set ℝ} (hs : UniqueDiffOn ℝ s) (hz : IsMIntegralCurveOn z (geodesicSpray I M) s) : IsGeodesicCurveOn I (fun (t : ℝ) => (z t).proj) s

The base curve of an integral curve of the geodesic spray is a geodesic. The integral curve equation supplies C² regularity within any parameter set with unique derivatives; no regularity of the projection needs to be assumed separately.

Regularity of geodesics

theorem TauCeti.Manifold.IsGeodesicCurveOn.contMDiffOn_curveVelocityLiftWithin_of_le {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {m k : WithTop ℕ∞} [I.Boundaryless] [IsManifold I 2 M] [IsManifold I m M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I k E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} (h : IsGeodesicCurveOn I γ s) (n : ℕ) (hm : ↑n + 2 ≤ m) (hk : ↑n + 1 ≤ k) : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I.tangent (↑n + 1) (curveVelocityLiftWithin I γ s) s

The velocity lift of a geodesic is C^(n + 1) on its parameter set, for a C^k metric on a C^m manifold with n + 1 ≤ k and n + 2 ≤ m. The parameter set only needs unique derivatives, so this includes the endpoints of a nondegenerate closed interval.

theorem TauCeti.Manifold.IsGeodesicCurveOn.contMDiffOn_of_le {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {m k : WithTop ℕ∞} [I.Boundaryless] [IsManifold I 2 M] [IsManifold I m M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I k E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} (h : IsGeodesicCurveOn I γ s) (n : ℕ) (hm : ↑n + 2 ≤ m) (hk : ↑n + 1 ≤ k) : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I (↑n + 2) γ s

A geodesic is C^(n + 2) on its parameter set, for a C^k metric on a C^m manifold with n + 1 ≤ k and n + 2 ≤ m.

theorem TauCeti.Manifold.IsGeodesicCurveOn.contMDiffOn_curveVelocityLiftWithin_infty {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [I.Boundaryless] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} (h : IsGeodesicCurveOn I γ s) : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I.tangent (↑⊤) (curveVelocityLiftWithin I γ s) s

The velocity lift of a geodesic of a smooth metric is smooth on its parameter set.

theorem TauCeti.Manifold.IsGeodesicCurveOn.contMDiffOn_infty {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [I.Boundaryless] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} (h : IsGeodesicCurveOn I γ s) : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I (↑⊤) γ s

Geodesics of a smooth metric are smooth. A geodesic, which is required only to be C², is C^∞ on its parameter set. The parameter set only needs unique derivatives, so this includes the endpoints of a nondegenerate closed interval.

theorem TauCeti.Manifold.IsGeodesicCurveOn.contMDiffAt_infty {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [I.Boundaryless] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} {t : ℝ} (h : IsGeodesicCurveOn I γ s) (ht : s ∈ nhds t) : ContMDiffAt (modelWithCornersSelf ℝ ℝ) I (↑⊤) γ t

A geodesic of a smooth metric is smooth at every interior point of its parameter set.

theorem TauCeti.Manifold.IsGeodesicCurve.contMDiff_infty {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [I.Boundaryless] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {γ : ℝ → M} (h : IsGeodesicCurve I γ) : ContMDiff (modelWithCornersSelf ℝ ℝ) I (↑⊤) γ

An all-time geodesic of a smooth metric is smooth.

theorem IsMIntegralCurveOn.isGeodesicCurveOnFrom_proj {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [I.Boundaryless] [IsManifold I 3 M] [IsContMDiffRiemannianBundle I 2 E fun (x : M) => TangentSpace I x] {z : ℝ → TangentBundle I M} {s : Set ℝ} {w : TangentBundle I M} (hz : IsMIntegralCurveOn z (TauCeti.Manifold.geodesicSpray I M) s) (hs : UniqueDiffOn ℝ s) (h0s : 0 ∈ s) (h0 : z 0 = w) : TauCeti.Manifold.IsGeodesicCurveOnFrom I (fun (t : ℝ) => (z t).proj) s w.proj w.snd

The projection of an integral curve of the geodesic spray on a parameter set with unique derivatives is the geodesic whose initial data are encoded by its value at zero.