Geodesics are the critical points of the energy

The first variation formula TauCeti.Manifold.IsFixedEndpointVariation.hasDerivAt_energy of TauCeti.Geometry.Manifold.Riemannian.FirstVariation.Basic expresses the derivative at s = 0 of the energy of a fixed-endpoint variation F of γ = F 0 as -∫_a^b ⟪V(t), D_t γ'(t)⟫ dt. This file proves the variational characterization of geodesics: on a boundaryless C^n manifold with 2 ≤ n ≤ ∞, a curve which is C^n near [a, b] is a critical point of the energy between a and b among C^n variations (TauCeti.Manifold.IsEnergyCritical) exactly when it is a geodesic on the open interval between a and b. In particular, for n = ∞, a smooth curve is critical among smooth variations with fixed endpoints exactly when it is a geodesic.

Along a geodesic the covariant acceleration D_t γ' vanishes, so the first variation vanishes. Conversely, suppose D_t γ'(t₀) ≠ 0 at an interior parameter t₀. In the extended chart at γ t₀, pushing γ in the direction of a fixed coordinate vector e, with a bump function φ supported near t₀ as profile, is a fixed-endpoint variation, as regular as γ and the manifold, whose variation field is φ times the coordinate field of e (TauCeti.Manifold.chartVariation). For e the coordinate vector of D_t γ'(t₀), the pairing g of that coordinate field with D_t γ' is positive at t₀; it is continuous there, because the first-variation integrand of such a variation is (TauCeti.Manifold.continuousAt_inner_variationField_acceleration). A bump supported where g > 0 then gives a variation whose first variation -∫_a^b φ g is nonzero.

Main definitions and results

• TauCeti.Manifold.IsGeodesicCurveOn.isEnergyCritical: geodesics are critical points of the energy among C^n variations with fixed endpoints, for every 2 ≤ n.
• TauCeti.Manifold.IsEnergyCritical.isGeodesicCurveOn: critical points of the energy are geodesics, for 2 ≤ n ≤ ∞.
• TauCeti.Manifold.isEnergyCritical_iff_isGeodesicCurveOn: the two combined.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 9, §2, Propositions 2.4 and 2.5.
• J. Milnor, Morse Theory, Annals of Mathematics Studies 51, Princeton, 1963, §12, Corollary 12.3.

Geodesics are critical

theorem TauCeti.Manifold.IsGeodesicCurveOn.isEnergyCritical {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} {a b : ℝ} [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 2 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {n : WithTop ℕ∞} (hn : 2 ≤ n) (h : IsGeodesicCurveOn I γ (Set.uIoo a b)) (hγ : ∀ t ∈ Set.uIcc a b, ContMDiffAt (modelWithCornersSelf ℝ ℝ) I n γ t) : IsEnergyCritical I n γ a b

Geodesics are critical points of the energy. For 2 ≤ n, a geodesic on the open interval between a and b which is C^n at every point of [a, b] is a critical point of the energy between a and b among C^n variations with fixed endpoints.

Critical points are geodesics

theorem TauCeti.Manifold.IsEnergyCritical.isGeodesicCurveOn {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} {a b : ℝ} {n : ℕ∞} [I.Boundaryless] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [IsManifold I (↑n) M] (hn : 2 ≤ n) (h : IsEnergyCritical I (↑n) γ a b) : IsGeodesicCurveOn I γ (Set.uIoo a b)

Critical points of the energy are geodesics. On a boundaryless C^n manifold with 2 ≤ n ≤ ∞, a critical point of the energy between a and b among C^n variations with fixed endpoints is a geodesic on the open interval between a and b. For n = ∞ this is the statement for smooth curves and smooth variations.

theorem TauCeti.Manifold.isEnergyCritical_iff_isGeodesicCurveOn {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} {a b : ℝ} {n : ℕ∞} [I.Boundaryless] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [IsManifold I (↑n) M] (hn : 2 ≤ n) (hγ : ∀ t ∈ Set.uIcc a b, ContMDiffAt (modelWithCornersSelf ℝ ℝ) I (↑n) γ t) : IsEnergyCritical I (↑n) γ a b ↔ IsGeodesicCurveOn I γ (Set.uIoo a b)

The variational characterization of geodesics. On a boundaryless C^n manifold with 2 ≤ n ≤ ∞, a curve which is C^n near every point of [a, b] is a critical point of the energy between a and b among C^n variations with fixed endpoints exactly when it is a geodesic on the open interval between a and b. For n = ∞: a smooth curve is critical among smooth variations exactly when it is a geodesic.