Existence of the negative gradient flow

The dynamical description of Morse theory reads its trajectory spaces off a flow: stable and unstable sets, and the Lyapunov theory of a decreasing function along trajectories, are statements about a Flow.IsNegativeGradient flow. This file produces such a flow for every function whose gradient is globally Lipschitz, by feeding -∇ f to TauCeti.flowOfLipschitz.

Global Lipschitz continuity of ∇ f is a sufficient hypothesis for the trajectories to exist for all time; it holds for instance whenever f is C² with a bounded second derivative, and in particular for the split quadratic model.

Throughout, ∇ f is Mathlib's gradient: a function defined for every f, taking the value 0 wherever f is not differentiable. What is constructed below is therefore the flow of the vector field -∇ f, and no differentiability of f is assumed for it, exactly as the predicate Flow.IsNegativeGradient it witnesses assumes none. Differentiability of f is what makes that field the gradient field of f, and it enters where the flow is used as a gradient flow rather than as the flow of a Lipschitz field: TauCeti.negativeGradientFlow_orbit_antitone records Lyapunov descent along any orbit on which f is differentiable.

Main declarations

• TauCeti.negativeGradientFlow: the negative gradient flow of a function with globally Lipschitz gradient.
• TauCeti.isNegativeGradient_negativeGradientFlow: it is a negative gradient flow of f.
• TauCeti.eq_negativeGradientFlow: every global negative gradient trajectory is one of its orbits.
• TauCeti.negativeGradientFlow_congr: it does not depend on the chosen Lipschitz bound.
• TauCeti.forall_negativeGradientFlow_eq_self_iff: its rest points are the zeros of ∇ f.
• TauCeti.negativeGradientFlow_orbit_antitone: f decreases along an orbit on which it is differentiable.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 2.

noncomputable def TauCeti.negativeGradientFlow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) {K : NNReal} (hf : LipschitzWith K (gradient f)) : Flow ℝ E

The negative gradient flow of a function whose gradient is globally Lipschitz.

This is the flow of the vector field -∇ f. For a differentiable f that field is the negative gradient field and this is the negative gradient flow in the usual sense; for an f that is not differentiable everywhere it is the flow of Mathlib's totalized gradient field, which is the object the hypothesis LipschitzWith K (∇ f) speaks about.

Equations

• TauCeti.negativeGradientFlow f hf = TauCeti.flowOfLipschitz (fun (x : E) => -gradient f x) ⋯

theorem TauCeti.isNegativeGradient_negativeGradientFlow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {K : NNReal} (f : E → ℝ) (hf : LipschitzWith K (gradient f)) : (negativeGradientFlow f hf).IsNegativeGradient f

The negative gradient flow is a negative gradient flow: each of its orbits solves γ' = -∇f(γ).

theorem TauCeti.eq_negativeGradientFlow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {K : NNReal} (f : E → ℝ) (hf : LipschitzWith K (gradient f)) {γ : ℝ → E} (hγ : IsIntegralCurve γ fun (x : ℝ) (y : E) => -gradient f y) (t : ℝ) : γ t = (negativeGradientFlow f hf).toFun t (γ 0)

Every global negative gradient trajectory is an orbit of the negative gradient flow.

theorem TauCeti.negativeGradientFlow_congr {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {K : NNReal} (f : E → ℝ) {K' : NNReal} (hf : LipschitzWith K (gradient f)) (hf' : LipschitzWith K' (gradient f)) : negativeGradientFlow f hf = negativeGradientFlow f hf'

Independence of the Lipschitz bound. Two Lipschitz witnesses for ∇ f, with possibly different constants, produce the same negative gradient flow.

theorem TauCeti.forall_negativeGradientFlow_eq_self_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {K : NNReal} (f : E → ℝ) (hf : LipschitzWith K (gradient f)) (x : E) : (∀ (t : ℝ), (negativeGradientFlow f hf).toFun t x = x) ↔ gradient f x = 0

The rest points of the negative gradient flow are the zeros of ∇ f, that is, the critical points of a differentiable f.

theorem TauCeti.negativeGradientFlow_orbit_antitone {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {K : NNReal} (f : E → ℝ) (hf : LipschitzWith K (gradient f)) (x : E) (hf' : ∀ (t : ℝ), DifferentiableAt ℝ f ((negativeGradientFlow f hf).toFun t x)) : Antitone fun (t : ℝ) => f ((negativeGradientFlow f hf).toFun t x)

Lyapunov descent along the negative gradient flow: a function decreases along any orbit on which it is differentiable. This is the point at which differentiability of f is needed, the construction of the flow itself only seeing the vector field -∇ f.