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.contDiff_negativeGradientFlow and TauCeti.contDiff_negativeGradientFlow_apply: for a globally C² function, this flow is C¹ jointly and at each fixed time.
• 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.isIntegralCurve_centeredNegativeGradientFlow: an orbit written in displacement coordinates solves the centred negative-gradient equation.
• TauCeti.flowOfLipschitz_centeredNegativeGradient_apply: identifies the flow of the centred field with the translated negative-gradient flow.
• TauCeti.eq_centeredNegativeGradientFlow_of_isIntegralCurveOn: uniqueness in displacement coordinates on a time set containing the interval from zero to the chosen time.
• 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.contDiff_negativeGradientFlow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {K : NNReal} (f : E → ℝ) (hf : LipschitzWith K (gradient f)) (hfs : ContDiff ℝ 2 f) : ContDiff ℝ 1 (Function.uncurry (negativeGradientFlow f hf).toFun)

The negative-gradient flow of a globally C² function is C¹, jointly in time and the initial condition. The global Lipschitz hypothesis supplies completeness of every orbit, while the two derivatives of f make its negative-gradient field C¹.

theorem TauCeti.contDiff_negativeGradientFlow_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {K : NNReal} (f : E → ℝ) (hf : LipschitzWith K (gradient f)) (hfs : ContDiff ℝ 2 f) (t : ℝ) : ContDiff ℝ 1 ((negativeGradientFlow f hf).toFun t)

At every fixed time, the negative-gradient flow of a globally C² function is C¹ in its initial condition.

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.lipschitzWith_centeredNegativeGradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {K : NNReal} (hf : LipschitzWith K (gradient f)) (x : E) : LipschitzWith K fun (z : E) => (-gradient f) (x + z)

Translating the negative-gradient field to displacement coordinates preserves its Lipschitz constant.

theorem TauCeti.isIntegralCurve_centeredNegativeGradientFlow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {K : NNReal} (hf : LipschitzWith K (gradient f)) (x z : E) : IsIntegralCurve (fun (t : ℝ) => (negativeGradientFlow f hf).toFun t (x + z) - x) fun (x_1 : ℝ) (w : E) => (-gradient f) (x + w)

A negative-gradient orbit, written in displacement coordinates about x, solves the centred negative-gradient equation.

theorem TauCeti.flowOfLipschitz_centeredNegativeGradient_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {K : NNReal} (hf : LipschitzWith K (gradient f)) (x z : E) (t : ℝ) : (flowOfLipschitz (fun (w : E) => (-gradient f) (x + w)) ⋯).toFun t z = (negativeGradientFlow f hf).toFun t (x + z) - x

The flow of the centred negative-gradient field is the negative-gradient flow translated to displacement coordinates.

theorem TauCeti.eq_centeredNegativeGradientFlow_of_isIntegralCurveOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {K : NNReal} (hf : LipschitzWith K (gradient f)) {x z : E} {y : ℝ → E} {s : Set ℝ} (hy : IsIntegralCurveOn y (fun (x_1 : ℝ) (w : E) => (-gradient f) (x + w)) s) (hy0 : y 0 = z) {t : ℝ} (hst : Set.uIcc 0 t ⊆ s) : y t = (negativeGradientFlow f hf).toFun t (x + z) - x

A centred negative-gradient trajectory on a time set containing the interval between zero and t is the corresponding translated orbit of the global negative-gradient flow at t.

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.