The energy of a curve

The energy of a curve γ in a Riemannian manifold between the parameters a and b is E(γ) = ½ ∫_a^b ‖γ'(t)‖² dt, where γ' is the velocity TauCeti.Manifold.curveVelocity. This file defines it and records its elementary properties: it vanishes on constant curves and on degenerate parameter intervals, changes sign under reversal of the parameter interval, and is nonnegative on positively oriented ones, and adds over adjacent parameter intervals. On a parameter set s containing the interval, it may equally be computed from the within-set velocity TauCeti.Manifold.curveVelocityWithin, which is the form used for geodesics on closed intervals, where the unrestricted velocity can take junk values at the endpoints. Its first variation is in TauCeti.Geometry.Manifold.Riemannian.FirstVariation.Basic, and its value on geodesic segments is in TauCeti.Geometry.Manifold.Riemannian.Geodesic.ConstantSpeed.

Main definitions and results

• TauCeti.Manifold.energy: the energy of a curve between two parameters.
• TauCeti.Manifold.energy_const, TauCeti.Manifold.energy_self: the energy vanishes on a constant curve and on a degenerate parameter interval.
• TauCeti.Manifold.energy_symm, TauCeti.Manifold.energy_nonneg: the energy is odd in the orientation of the parameter interval and nonnegative on positively oriented ones.
• TauCeti.Manifold.energy_add_adjacent: the energy is additive over adjacent parameter intervals.
• TauCeti.Manifold.energy_congr: energy depends only on the open-interval restriction.
• TauCeti.Manifold.sum_energy_adjacent_intervals: energy is additive over finite partitions.
• TauCeti.Manifold.energy_eq_integral_curveVelocityWithin: the energy computed from the velocity within any parameter set containing the interval.

References

• J. Milnor, Morse Theory, Annals of Mathematics Studies 51, Princeton, 1963, §12, the energy of a path.
• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 9, §2.

noncomputable def TauCeti.Manifold.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] (γ : ℝ → M) (a b : ℝ) : ℝ

The energy of a curve γ between the parameters a and b: half the integral of its squared Riemannian speed, E(γ) = ½ ∫_a^b ‖γ'(t)‖² dt. It is meant for curves which are C¹ near [a, b]; for other curves the integrand may take junk values.

theorem TauCeti.Manifold.energy_def {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] (γ : ℝ → M) (a b : ℝ) : energy I γ a b = (∫ (t : ℝ) in a..b, ‖curveVelocity I γ t‖ ^ 2) / 2

The defining formula for the energy.

@[simp]

theorem TauCeti.Manifold.energy_const {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] (x : M) (a b : ℝ) : energy I (fun (x_1 : ℝ) => x) a b = 0

A constant curve has zero energy.

@[simp]

theorem TauCeti.Manifold.energy_self {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] (γ : ℝ → M) (a : ℝ) : energy I γ a a = 0

The energy over a degenerate parameter interval vanishes.

theorem TauCeti.Manifold.energy_symm {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] (γ : ℝ → M) (a b : ℝ) : energy I γ b a = -energy I γ a b

Reversing the parameter interval changes the sign of the energy.

theorem TauCeti.Manifold.energy_nonneg {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] (γ : ℝ → M) {a b : ℝ} (hab : a ≤ b) : 0 ≤ energy I γ a b

The energy over a positively oriented parameter interval is nonnegative.

theorem TauCeti.Manifold.energy_add_adjacent {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] (γ : ℝ → M) {a b c : ℝ} (hab : IntervalIntegrable (fun (t : ℝ) => ‖curveVelocity I γ t‖ ^ 2) MeasureTheory.volume a b) (hbc : IntervalIntegrable (fun (t : ℝ) => ‖curveVelocity I γ t‖ ^ 2) MeasureTheory.volume b c) : energy I γ a b + energy I γ b c = energy I γ a c

The energy is additive over adjacent parameter intervals, provided the squared speed is integrable on both.

theorem Filter.EventuallyEq.norm_curveVelocity_eq {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] {γ δ : ℝ → M} {t : ℝ} (h : γ =ᶠ[nhds t] δ) : ‖TauCeti.Manifold.curveVelocity I γ t‖ = ‖TauCeti.Manifold.curveVelocity I δ t‖

Curves agreeing near a parameter have the same Riemannian speed there.

theorem TauCeti.Manifold.energy_congr {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] {γ δ : ℝ → M} {a b : ℝ} (h : Set.EqOn γ δ (Set.uIoo a b)) : energy I γ a b = energy I δ a b

Energy depends only on the curve on the open parameter interval; values at its endpoints and outside the interval do not affect the integral.

theorem TauCeti.Manifold.sum_energy_adjacent_intervals {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] (γ : ℝ → M) {n : ℕ} (τ : Fin (n + 1) → ℝ) (hint : ∀ (i : Fin n), IntervalIntegrable (fun (t : ℝ) => ‖curveVelocity I γ t‖ ^ 2) MeasureTheory.volume (τ i.castSucc) (τ i.succ)) : ∑ i : Fin n, energy I γ (τ i.castSucc) (τ i.succ) = energy I γ (τ 0) (τ (Fin.last n))

Energy is additive over any finite partition on which the squared speed is integrable. The partition need not be strict or increasing.

theorem TauCeti.Manifold.energy_eq_integral_curveVelocityWithin {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] (γ : ℝ → M) {s : Set ℝ} {a b : ℝ} (hs : Set.uIcc a b ⊆ s) : energy I γ a b = (∫ (t : ℝ) in a..b, ‖curveVelocityWithin I γ s t‖ ^ 2) / 2

On any parameter set s containing the interval between a and b, the energy may be computed from the velocity within s. The two velocities agree on the open interval, so no regularity of γ is needed.