Finite energy of negative gradient trajectories

For a negative gradient trajectory whose function values converge at both ends, the squared norm of the gradient is integrable on the whole real line, and its integral is the difference of the limiting values. Integrability is a conclusion, not an assumption. No continuity of the gradient or nondegeneracy of the limiting points is required: the nonnegative derivative of -f ∘ γ is automatically integrable on compact intervals, and convergence of its primitive controls the improper integrals.

The half-line formulas identify the energy remaining before or after any time. Mathlib's MeasureTheory.tendsto_integral_Iic_zero and MeasureTheory.tendsto_integral_Ioi_zero give the vanishing of these tails. Together with TauCeti.IsIntegralCurveOn.exists_tendsto_comp_atTop from Morse.Convergence, the forward integrability theorem gives finite energy for a negative gradient trajectory confined to a compact set. The forward and backward critical-point convergence theorems in that module similarly supply the limits for the whole-line identity. For a connecting orbit from p to q, the total energy is f p - f q; in particular it depends only on the endpoints. These energy formulas apply to the trajectories themselves, without manifold structures on their stable and unstable sets.

Apply the trajectory lemmas by their qualified names in TauCeti.IsIntegralCurveOn and TauCeti.IsIntegralCurve, following the organization of Morse.GradientFlow. The curve predicates themselves are Mathlib's IsIntegralCurveOn and IsIntegralCurve; the qualified namespaces above contain the energy lemmas, not new predicates. The connecting-orbit lemmas are in TauCeti.Flow.IsNegativeGradient. With open TauCeti, use hφ.integrable_norm_gradient_sq_of_mem_unstableSet_inter_stableSet hf hfp hfq hx for finite energy, and hφ.integral_norm_gradient_sq_eq_sub_of_mem_unstableSet_inter_stableSet hf hfp hfq hx for the endpoint energy identity. The restricted-curve lemmas take the interval endpoints before the curve hypothesis; for example, TauCeti.IsIntegralCurveOn.integrableOn_Ioi_norm_gradient_sq a hγ hf hplus proves finite forward energy after time a.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 2 (gradient trajectories) and Section 6.5.a (their energy).

The improper-integral arguments use Mathlib's nonnegative-derivative FTC and MeasureTheory.integrableOn_Iic_of_intervalIntegral_norm_tendsto.

theorem TauCeti.IsIntegralCurveOn.intervalIntegrable_norm_gradient_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} (a b : ℝ) (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.uIcc a b)) (hf : ∀ t ∈ Set.uIcc a b, DifferentiableAt ℝ f (γ t)) : IntervalIntegrable (fun (t : ℝ) => ‖gradient f (γ t)‖ ^ 2) MeasureTheory.volume a b

The squared gradient along a negative gradient trajectory is integrable on every compact time interval, assuming only differentiability of the defining function along that interval.

theorem TauCeti.IsIntegralCurveOn.integrableOn_Ioi_norm_gradient_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {cPlus : ℝ} (a : ℝ) (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Ici a)) (hf : ∀ t ∈ Set.Ici a, DifferentiableAt ℝ f (γ t)) (hplus : Filter.Tendsto (f ∘ γ) Filter.atTop (nhds cPlus)) : MeasureTheory.IntegrableOn (fun (t : ℝ) => ‖gradient f (γ t)‖ ^ 2) (Set.Ioi a) MeasureTheory.volume

A finite forward limiting value implies finite energy on every forward half-line.

theorem TauCeti.IsIntegralCurveOn.integral_Ioi_norm_gradient_sq_eq_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {cPlus : ℝ} (a : ℝ) (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Ici a)) (hf : ∀ t ∈ Set.Ici a, DifferentiableAt ℝ f (γ t)) (hplus : Filter.Tendsto (f ∘ γ) Filter.atTop (nhds cPlus)) : ∫ (t : ℝ) in Set.Ioi a, ‖gradient f (γ t)‖ ^ 2 = f (γ a) - cPlus

The energy after time a is the drop from the value at a to the forward limiting value.

theorem TauCeti.IsIntegralCurveOn.integrableOn_Iic_norm_gradient_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {cMinus : ℝ} (a : ℝ) (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Iic a)) (hf : ∀ t ∈ Set.Iic a, DifferentiableAt ℝ f (γ t)) (hminus : Filter.Tendsto (f ∘ γ) Filter.atBot (nhds cMinus)) : MeasureTheory.IntegrableOn (fun (t : ℝ) => ‖gradient f (γ t)‖ ^ 2) (Set.Iic a) MeasureTheory.volume

A finite backward limiting value implies finite energy on every backward half-line.

theorem TauCeti.IsIntegralCurveOn.integral_Iic_norm_gradient_sq_eq_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {cMinus : ℝ} (a : ℝ) (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Iic a)) (hf : ∀ t ∈ Set.Iic a, DifferentiableAt ℝ f (γ t)) (hminus : Filter.Tendsto (f ∘ γ) Filter.atBot (nhds cMinus)) : ∫ (t : ℝ) in Set.Iic a, ‖gradient f (γ t)‖ ^ 2 = cMinus - f (γ a)

The energy before time a is the drop from the backward limiting value to the value at a.

theorem TauCeti.IsIntegralCurve.integrable_norm_gradient_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {cMinus cPlus : ℝ} (hγ : IsIntegralCurve γ fun (x : ℝ) (x_1 : E) => -gradient f x_1) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (γ t)) (hminus : Filter.Tendsto (f ∘ γ) Filter.atBot (nhds cMinus)) (hplus : Filter.Tendsto (f ∘ γ) Filter.atTop (nhds cPlus)) : MeasureTheory.Integrable (fun (t : ℝ) => ‖gradient f (γ t)‖ ^ 2) MeasureTheory.volume

A negative gradient trajectory with finite limiting values at both ends has finite total energy. Neither continuity of the gradient nor nondegeneracy of the endpoints is needed.

theorem TauCeti.IsIntegralCurve.integral_norm_gradient_sq_eq_sub_of_tendsto {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {cMinus cPlus : ℝ} (hγ : IsIntegralCurve γ fun (x : ℝ) (x_1 : E) => -gradient f x_1) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (γ t)) (hminus : Filter.Tendsto (f ∘ γ) Filter.atBot (nhds cMinus)) (hplus : Filter.Tendsto (f ∘ γ) Filter.atTop (nhds cPlus)) : ∫ (t : ℝ), ‖gradient f (γ t)‖ ^ 2 = cMinus - cPlus

Total energy identity. The energy of a negative gradient trajectory with finite limiting values at both ends equals their difference. Integrability is proved from these limits.

theorem TauCeti.Flow.IsNegativeGradient.integrable_norm_gradient_sq_of_mem_unstableSet_inter_stableSet {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} {p q x : E} (hφ : φ.IsNegativeGradient f) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (φ.toFun t x)) (hfp : ContinuousAt f p) (hfq : ContinuousAt f q) (hx : x ∈ φ.unstableSet p ∩ φ.stableSet q) : MeasureTheory.Integrable (fun (t : ℝ) => ‖gradient f (φ.toFun t x)‖ ^ 2) MeasureTheory.volume

Every orbit connecting p to q has integrable squared gradient.

theorem TauCeti.Flow.IsNegativeGradient.integral_norm_gradient_sq_eq_sub_of_mem_unstableSet_inter_stableSet {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} {p q x : E} (hφ : φ.IsNegativeGradient f) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (φ.toFun t x)) (hfp : ContinuousAt f p) (hfq : ContinuousAt f q) (hx : x ∈ φ.unstableSet p ∩ φ.stableSet q) : ∫ (t : ℝ), ‖gradient f (φ.toFun t x)‖ ^ 2 = f p - f q

Every orbit connecting p to q has total energy f p - f q.