The first variation of energy

The energy E(γ) = ½ ∫_a^b ‖γ'(t)‖² dt of a curve γ in a Riemannian manifold between the parameters a and b is TauCeti.Manifold.energy, defined in TauCeti.Geometry.Manifold.Riemannian.Energy. A variation of γ is a two-parameter family F with F 0 = γ, with variation field V = TauCeti.Manifold.variationField I F, the transverse velocity V(t) = ∂F/∂s (0, t). This file computes the derivative at s = 0 of the energy of the curves F s:

d/ds E(F s) |₀ = ⟪V(b), γ'(b)⟫ - ⟪V(a), γ'(a)⟫ - ∫_a^b ⟪V(t), D_t γ'(t)⟫ dt,

where D_t γ' is the covariant acceleration of γ for the Levi-Civita connection. When the curves near s = 0 share the endpoints of γ, the boundary terms vanish. The same formula holds at every parameter u of the family, with γ = F u and V(t) = ∂F/∂s (u, t).

The formula holds for a family which is C² at the points of {0} × [a, b], for the tangent bundle of a C² manifold carrying a C¹ Riemannian metric; its integrand is then continuous on [a, b]. It is the tool for studying the critical points of the energy, the C^n curves for which this derivative vanishes for every C^n variation with fixed endpoints (TauCeti.Manifold.IsFixedEndpointVariation), for a regularity 2 ≤ n. On a boundaryless C^n manifold, for 2 ≤ n ≤ ∞, a C^n curve is critical exactly when it is a geodesic on uIoo a b (TauCeti.Geometry.Manifold.Riemannian.Geodesic.FirstVariation).

Main definitions and results

• TauCeti.Manifold.hasDerivAt_energy: the first variation formula for the energy, with boundary terms.
• TauCeti.Manifold.IsFixedEndpointVariation.hasDerivAt_energy: the first variation formula for a C² variation with fixed endpoints.
• TauCeti.Manifold.hasDerivAt_energy_curveVelocity_fst: the first variation formula at any parameter u of the family, and TauCeti.Manifold.eventually_differentiableAt_energy: the energy of F s is differentiable for s near any parameter u at which F is C² along {u} × [a, b].
• TauCeti.Manifold.continuousAt_inner_variationField_acceleration: the integrand ⟪V(t), D_t γ'(t)⟫ of the first variation formula is continuous where the family is C².
• TauCeti.Manifold.IsEnergyCritical: critical points of the energy among C^n variations with fixed endpoints, which are C^n curves by definition; for 2 ≤ n, criticality is characterized through the first variation formula by TauCeti.Manifold.isEnergyCritical_iff_integral_inner_eq_zero.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 9, §2, Proposition 2.4.
• J. Milnor, Morse Theory, Annals of Mathematics Studies 51, Princeton, 1963, §12, the energy of a path and its first variation.
• J. M. Lee, Introduction to Riemannian Manifolds, GTM 176, 2nd ed., 2018, Ch. 6, the first variation formula for length, whose proof follows the same scheme.

The first variation of energy

theorem TauCeti.Manifold.continuousAt_inner_variationField_acceleration {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : ℝ → ℝ → M} [FiniteDimensional ℝ E] [IsManifold I 2 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {t : ℝ} (hf : ContMDiffAt (modelWithCornersSelf ℝ (ℝ × ℝ)) I 2 (fun (z : ℝ × ℝ) => F z.1 z.2) (0, t)) : ContinuousAt (fun (r : ℝ) => inner ℝ (variationField I F r) ((CovariantDerivative.leviCivitaConnection I M).acceleration (F 0) r)) t

Continuity of the first-variation integrand. At a parameter t where the family is C², the integrand r ↦ ⟪V(r), D_r γ'(r)⟫ of the first variation formula is continuous, where V is the variation field and D_r γ' is the covariant acceleration of γ = F 0.

theorem TauCeti.Manifold.hasDerivAt_energy {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : ℝ → ℝ → M} [FiniteDimensional ℝ E] [IsManifold I 2 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {a b : ℝ} (hF : ∀ t ∈ Set.uIcc a b, ContMDiffAt (modelWithCornersSelf ℝ (ℝ × ℝ)) I 2 (fun (z : ℝ × ℝ) => F z.1 z.2) (0, t)) : HasDerivAt (fun (s : ℝ) => energy I (F s) a b) (inner ℝ (variationField I F b) (curveVelocity I (F 0) b) - inner ℝ (variationField I F a) (curveVelocity I (F 0) a) - ∫ (t : ℝ) in a..b, inner ℝ (variationField I F t) ((CovariantDerivative.leviCivitaConnection I M).acceleration (F 0) t)) 0

The first variation of energy. Let F be a two-parameter family which is C² at every point of {0} × [a, b], with central curve γ = F 0 and variation field V. Then the energy of F s between a and b is differentiable at s = 0, with derivative

⟪V(b), γ'(b)⟫ - ⟪V(a), γ'(a)⟫ - ∫_a^b ⟪V(t), D_t γ'(t)⟫ dt,

where D_t γ' is the covariant acceleration of γ for the Levi-Civita connection.

theorem TauCeti.Manifold.IsFixedEndpointVariation.hasDerivAt_energy {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : ℝ → ℝ → M} [FiniteDimensional ℝ E] [IsManifold I 2 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {a b : ℝ} (hF : IsFixedEndpointVariation I 2 F a b) : HasDerivAt (fun (s : ℝ) => energy I (F s) a b) (-∫ (t : ℝ) in a..b, inner ℝ (variationField I F t) ((CovariantDerivative.leviCivitaConnection I M).acceleration (F 0) t)) 0

The first variation of energy for a variation with fixed endpoints. For a C² variation F of γ = F 0 with fixed endpoints between a and b, the derivative at s = 0 of the energy is -∫_a^b ⟪V(t), D_t γ'(t)⟫ dt.

theorem TauCeti.Manifold.hasDerivAt_energy_curveVelocity_fst {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : ℝ → ℝ → M} [FiniteDimensional ℝ E] [IsManifold I 2 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {a b u : ℝ} (hF : ∀ t ∈ Set.uIcc a b, ContMDiffAt (modelWithCornersSelf ℝ (ℝ × ℝ)) I 2 (fun (z : ℝ × ℝ) => F z.1 z.2) (u, t)) : HasDerivAt (fun (s : ℝ) => energy I (F s) a b) (inner ℝ (curveVelocity I (fun (q : ℝ) => F q b) u) (curveVelocity I (F u) b) - inner ℝ (curveVelocity I (fun (q : ℝ) => F q a) u) (curveVelocity I (F u) a) - ∫ (t : ℝ) in a..b, inner ℝ (curveVelocity I (fun (q : ℝ) => F q t) u) ((CovariantDerivative.leviCivitaConnection I M).acceleration (F u) t)) u

The first variation of energy at any parameter of the family. Let F be a two-parameter family which is C² at every point of {u} × [a, b], and let γ = F u. Then the energy of F s between a and b is differentiable at s = u, with derivative

⟪W(b), γ'(b)⟫ - ⟪W(a), γ'(a)⟫ - ∫_a^b ⟪W(t), D_t γ'(t)⟫ dt,

where W(t) = ∂F/∂s (u, t) is the velocity at u of the transverse curve q ↦ F q t. For u = 0, W is the variation field and this is TauCeti.Manifold.hasDerivAt_energy.

theorem TauCeti.Manifold.eventually_differentiableAt_energy {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : ℝ → ℝ → M} [FiniteDimensional ℝ E] [IsManifold I 2 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {a b u : ℝ} (hF : ∀ t ∈ Set.uIcc a b, ContMDiffAt (modelWithCornersSelf ℝ (ℝ × ℝ)) I 2 (fun (z : ℝ × ℝ) => F z.1 z.2) (u, t)) : ∀ᶠ (s : ℝ) in nhds u, DifferentiableAt ℝ (fun (s : ℝ) => energy I (F s) a b) s

If a two-parameter family is C² at every point of {u} × [a, b], then the energy of F s between a and b is differentiable at every s near u.

Critical points of the energy

structure TauCeti.Manifold.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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (n : WithTop ℕ∞) (γ : ℝ → M) (a b : ℝ) : Prop

A curve γ is a critical point of the energy among C^n variations between the parameters a and b when it is C^n at every point of [a, b] and every C^n variation of γ with fixed endpoints leaves the energy stationary to first order: for every C^n fixed-endpoint variation F between a and b (TauCeti.Manifold.IsFixedEndpointVariation) with F 0 = γ, the energy of F s between a and b has derivative 0 at s = 0. The regularity of γ is part of the definition: a curve which is not C^n on [a, b] admits no such variation, and is not critical.

The regularity n is meant to be at least 2, where the first variation formula applies; the usual notion is n = ∞, criticality of a smooth curve among smooth variations. On a boundaryless C^n manifold, for 2 ≤ n ≤ ∞, a curve which is C^n on [a, b] is critical exactly when it is a geodesic; this is TauCeti.Manifold.isEnergyCritical_iff_isGeodesicCurveOn in TauCeti.Geometry.Manifold.Riemannian.Geodesic.FirstVariation. Hence, on a boundaryless C^n manifold with n ≤ ∞, criticality among C^m variations is the same for every 2 ≤ m ≤ n, for curves which are C^n on [a, b]; it is not independent of the regularity in general, since it requires γ itself to be C^m.

• contMDiffAt (t : ℝ) : t ∈ Set.uIcc a b → ContMDiffAt (modelWithCornersSelf ℝ ℝ) I n γ t

  A critical point of the energy among C^n variations is C^n at every point of [a, b].

• hasDerivAt {F : ℝ → ℝ → M} : F 0 = γ → IsFixedEndpointVariation I n F a b → HasDerivAt (fun (s : ℝ) => energy I (F s) a b) 0 0

  The energy of a C^n fixed-endpoint variation of a critical point has derivative 0 at s = 0.

theorem TauCeti.Manifold.isEnergyCritical_iff_integral_inner_eq_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] [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 ℕ∞} {γ : ℝ → M} {a b : ℝ} (hn : 2 ≤ n) (hγ : ∀ t ∈ Set.uIcc a b, ContMDiffAt (modelWithCornersSelf ℝ ℝ) I n γ t) : IsEnergyCritical I n γ a b ↔ ∀ (F : ℝ → ℝ → M), F 0 = γ → IsFixedEndpointVariation I n F a b → ∫ (t : ℝ) in a..b, inner ℝ (variationField I F t) ((CovariantDerivative.leviCivitaConnection I M).acceleration (F 0) t) = 0

Criticality through the first variation formula. For 2 ≤ n, a curve γ which is C^n at every point of [a, b] is a critical point of the energy among C^n variations between a and b exactly when ∫_a^b ⟪V(t), D_t γ'(t)⟫ dt = 0 for the variation field V of every C^n variation F of γ = F 0 with fixed endpoints between a and b.