Negative gradient trajectories

This file develops the first dynamical facts about negative gradient trajectories in a real Hilbert space. A curve γ is read through Mathlib's existing IsIntegralCurveOn predicate for the autonomous vector field fun _ x ↦ -∇ f x; no parallel notion of trajectory is introduced.

The basic calculation is

d/dt f(γ(t)) = -‖∇f(γ(t))‖².

It makes f a Lyapunov function: f ∘ γ is antitone, and strictly antitone on any interval on which the trajectory contains no critical point. Integrating the calculation gives the energy identity

∫ t in a..b, ‖∇f(γ(t))‖² = f(γ(a)) - f(γ(b)).

In particular a periodic negative gradient trajectory is stationary in the dynamical sense that its gradient vanishes at every point of the curve. These statements are the entry point to the gradient-flow, stable/unstable-manifold, and broken-trajectory constructions in the dynamical route to Morse homology.

Main results

• TauCeti.isIntegralCurve_const_neg_gradient_iff: the constant curves are precisely the critical points of the vector field.
• TauCeti.IsIntegralCurveOn.hasDerivWithinAt_comp_neg_gradient: derivative of f along a negative gradient trajectory.
• TauCeti.IsIntegralCurveOn.antitoneOn_comp_neg_gradient and TauCeti.IsIntegralCurveOn.strictAntiOn_comp_neg_gradient: Lyapunov monotonicity and strict descent away from critical points.
• TauCeti.IsIntegralCurveOn.integral_norm_gradient_sq_eq_sub and TauCeti.IsIntegralCurve.integral_norm_gradient_sq_eq_sub: the energy identity.
• TauCeti.IsIntegralCurve.gradient_eq_zero_of_eventually_const_value: a trajectory on which f is eventually constant passes through critical points.
• TauCeti.IsIntegralCurve.gradient_eq_zero_of_periodic and TauCeti.IsIntegralCurve.eq_of_periodic_neg_gradient: a periodic negative gradient trajectory consists entirely of critical points and is constant.
• Flow.IsNegativeGradient: every orbit of a flow solves the negative gradient equation.
• Flow.isNegativeGradient_iff: the introduction and elimination rule for that predicate.
• Flow.IsNegativeGradient.isIntegralCurve: the orbit curve through a point, as an integral curve of the negative gradient field.
• Flow.IsNegativeGradient.orbit_antitone: the defining function is antitone along every orbit of its negative gradient flow.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 2.
• Heegaard Floer homology roadmap, Lane M, "Morse homology".

@[simp]

theorem TauCeti.isIntegralCurve_const_neg_gradient_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} : (IsIntegralCurve (fun (x_1 : ℝ) => x) fun (x : ℝ) (y : E) => -gradient f y) ↔ gradient f x = 0

A constant curve is an integral curve of the negative gradient field exactly when its value is a critical point of that field.

theorem TauCeti.IsIntegralCurveOn.hasDerivWithinAt_comp_neg_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {s : Set ℝ} {t : ℝ} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) s) (ht : t ∈ s) (hf : DifferentiableAt ℝ f (γ t)) : HasDerivWithinAt (f ∘ γ) (-‖gradient f (γ t)‖ ^ 2) s t

Along a negative gradient trajectory, the derivative of f is the negative squared norm of its gradient. This within-set form is the one used for trajectories on their maximal interval of definition.

theorem TauCeti.IsIntegralCurveOn.antitoneOn_comp_neg_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {s : Set ℝ} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) s) (hs : Convex ℝ s) (hf : ∀ t ∈ s, DifferentiableAt ℝ f (γ t)) : AntitoneOn (f ∘ γ) s

The value of f is antitone along a negative gradient trajectory on a convex time domain.

theorem TauCeti.IsIntegralCurveOn.strictAntiOn_comp_neg_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {s : Set ℝ} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) s) (hs : Convex ℝ s) (hf : ∀ t ∈ s, DifferentiableAt ℝ f (γ t)) (hcrit : ∀ t ∈ interior s, gradient f (γ t) ≠ 0) : StrictAntiOn (f ∘ γ) s

Away from critical points, the value of f is strictly decreasing along a negative gradient trajectory on a convex time domain.

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

Energy identity for a negative gradient trajectory. Between two times of the trajectory's time domain, the drop in f equals the integral of the squared norm of its gradient along the trajectory.

theorem TauCeti.IsIntegralCurve.hasDerivAt_comp_neg_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {t : ℝ} (hγ : IsIntegralCurve γ fun (x : ℝ) (x_1 : E) => -gradient f x_1) (hf : DifferentiableAt ℝ f (γ t)) : HasDerivAt (f ∘ γ) (-‖gradient f (γ t)‖ ^ 2) t

Along a global negative gradient trajectory, the derivative of f is the negative squared norm of its gradient.

theorem TauCeti.IsIntegralCurve.antitone_comp_neg_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} (hγ : IsIntegralCurve γ fun (x : ℝ) (x_1 : E) => -gradient f x_1) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (γ t)) : Antitone (f ∘ γ)

The value of f is antitone along a global negative gradient trajectory.

theorem TauCeti.IsIntegralCurve.strictAnti_comp_neg_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} (hγ : IsIntegralCurve γ fun (x : ℝ) (x_1 : E) => -gradient f x_1) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (γ t)) (hcrit : ∀ (t : ℝ), gradient f (γ t) ≠ 0) : StrictAnti (f ∘ γ)

If a global negative gradient trajectory contains no critical point, then the value of f is strictly decreasing along it.

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

Energy identity for a global negative gradient trajectory. The drop in f between two times equals the integral of the squared norm of its gradient along the trajectory.

theorem TauCeti.IsIntegralCurve.gradient_eq_zero_of_eventually_const_value {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {t : ℝ} (hγ : IsIntegralCurve γ fun (x : ℝ) (x_1 : E) => -gradient f x_1) (hf : DifferentiableAt ℝ f (γ t)) {c : ℝ} (hval : ∀ᶠ (u : ℝ) in nhds t, f (γ u) = c) : gradient f (γ t) = 0

If the value of f is eventually constant along a global negative gradient trajectory, then the gradient of f vanishes at the corresponding point.

theorem TauCeti.IsIntegralCurve.gradient_eq_zero_of_periodic {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} (hγ : IsIntegralCurve γ fun (x : ℝ) (x_1 : E) => -gradient f x_1) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (γ t)) {T : ℝ} (hT : 0 < T) (hper : Function.Periodic γ T) (t : ℝ) : gradient f (γ t) = 0

A periodic negative gradient trajectory consists entirely of critical points. Thus negative gradient dynamics has no nonconstant periodic orbit.

theorem TauCeti.IsIntegralCurve.eq_of_periodic_neg_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} (hγ : IsIntegralCurve γ fun (x : ℝ) (x_1 : E) => -gradient f x_1) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (γ t)) {T : ℝ} (hT : 0 < T) (hper : Function.Periodic γ T) (t u : ℝ) : γ t = γ u

A periodic negative gradient trajectory is constant.

def Flow.IsNegativeGradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (φ : Flow ℝ E) (f : E → ℝ) : Prop

A real flow is the negative gradient flow of f when each of its orbit curves solves γ' = -∇f(γ). Regularity and uniqueness assumptions used to construct the flow remain separate; this predicate records precisely the differential equation needed by its dynamical consequences.

Equations

• φ.IsNegativeGradient f = ∀ (x : E), IsIntegralCurve (fun (t : ℝ) => φ.toFun t x) fun (x : ℝ) (y : E) => -gradient f y

theorem Flow.isNegativeGradient_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} : φ.IsNegativeGradient f ↔ ∀ (x : E), IsIntegralCurve (fun (t : ℝ) => φ.toFun t x) fun (x : ℝ) (y : E) => -gradient f y

The introduction and elimination rule for a negative-gradient flow.

theorem Flow.IsNegativeGradient.isIntegralCurve {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} (hφ : φ.IsNegativeGradient f) (x : E) : IsIntegralCurve (fun (t : ℝ) => φ.toFun t x) fun (x : ℝ) (y : E) => -gradient f y

Each orbit curve of a negative gradient flow solves the negative gradient equation.

theorem Flow.IsNegativeGradient.orbit_antitone {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} (hφ : φ.IsNegativeGradient f) (x : E) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (φ.toFun t x)) : Antitone fun (t : ℝ) => f (φ.toFun t x)

The defining function is antitone along every orbit of its negative gradient flow.