Stable and unstable sets of a negative gradient flow

This file specializes stable and unstable sets to a flow whose trajectories solve the negative gradient equation. Along such a flow the defining function is antitone. Consequently, a point in the stable set of q has value at least f q, while a point in the unstable set of p has value at most f p.

The intersection unstableSet φ p ∩ stableSet φ q is the set underlying the parametrized Morse trajectories from p to q. It is empty unless f q ≤ f p; when p ≠ q, the inequality is strict. In particular a negative gradient flow has no nonconstant homoclinic trajectories.

Reversing time turns a negative gradient flow of f into one of -f, exchanging the stable and unstable sets. An energy barrier confines trajectories: if ‖∇ f‖ ≥ c on an annulus about x, a trajectory converging to x cannot cross the annulus unless it starts at least c times the width of the annulus above f x. This is what makes the stable set agree, near a nondegenerate critical point, with the set of trajectories confined to a small ball, and hence what makes it an embedded submanifold (TauCeti.Analysis.Calculus.Morse.GlobalChart).

Main declarations

• Flow.IsNegativeGradient.value_le_of_mem_stableSet: stable-set points lie above the limiting critical value.
• Flow.IsNegativeGradient.value_ge_of_mem_unstableSet: unstable-set points lie below the limiting critical value.
• Flow.IsNegativeGradient.value_le_of_mem_unstableSet_inter_stableSet: a connecting trajectory goes from a weakly higher critical value to a lower one.
• Flow.IsNegativeGradient.value_lt_of_mem_unstableSet_inter_stableSet: the inequality is strict for distinct endpoints.
• Flow.IsNegativeGradient.eq_of_mem_unstableSet_inter_stableSet: there are no nonconstant homoclinic trajectories.
• Flow.IsNegativeGradient.reverse: the reversed flow is a negative gradient flow of -f.
• Flow.IsNegativeGradient.dist_le_of_mem_stableSet and Flow.IsNegativeGradient.dist_le_of_mem_unstableSet: the energy barrier confining stable and unstable trajectories that start low enough near their limit.

References

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

theorem Flow.IsNegativeGradient.value_le_of_mem_stableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} {p x : E} (hφ : φ.IsNegativeGradient f) (hx : x ∈ φ.stableSet p) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (φ.toFun t x)) (hfp : ContinuousAt f p) : f p ≤ f x

A point in the stable set of p has value at least f p. Only differentiability along the chosen orbit and continuity at its limiting point are required.

theorem Flow.IsNegativeGradient.value_ge_of_mem_unstableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} {p x : E} (hφ : φ.IsNegativeGradient f) (hx : x ∈ φ.unstableSet p) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (φ.toFun t x)) (hfp : ContinuousAt f p) : f x ≤ f p

A point in the unstable set of p has value at most f p. Only differentiability along the chosen orbit and continuity at its limiting point are required.

theorem Flow.IsNegativeGradient.value_le_of_mem_unstableSet_inter_stableSet {E : Type u_1} [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) : f q ≤ f p

If an orbit converges to p in backward time and to q in forward time, then f q ≤ f p.

theorem Flow.IsNegativeGradient.eq_of_mem_unstableSet_inter_stableSet_of_value_eq {E : Type u_1} [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) (hpq : f p = f q) : x = p ∧ p = q

A connecting orbit whose two endpoint values agree lies on the constant orbit through the shared endpoint: x = p and p = q.

theorem Flow.IsNegativeGradient.value_lt_of_mem_unstableSet_inter_stableSet {E : Type u_1} [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) (hpq : p ≠ q) (hx : x ∈ φ.unstableSet p ∩ φ.stableSet q) : f q < f p

A negative gradient connecting orbit between distinct endpoints strictly lowers the defining function.

theorem Flow.IsNegativeGradient.eq_of_mem_unstableSet_inter_stableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} {p x : E} (hφ : φ.IsNegativeGradient f) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (φ.toFun t x)) (hfp : ContinuousAt f p) (hx : x ∈ φ.unstableSet p ∩ φ.stableSet p) : x = p

A point lying in both the stable and unstable set of the same endpoint lies on the constant orbit of that endpoint. Thus a negative gradient flow has no nonconstant homoclinic orbit.

theorem Flow.IsNegativeGradient.reverse {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} (hφ : φ.IsNegativeGradient f) : φ.reverse.IsNegativeGradient (-f)

Reversing time turns a negative gradient flow of f into a negative gradient flow of -f.

theorem Flow.IsNegativeGradient.dist_le_of_mem_stableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} {x z : E} (hφ : φ.IsNegativeGradient f) (hz : z ∈ φ.stableSet x) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (φ.toFun t z)) (hfx : ContinuousAt f x) {s r c : ℝ} (hc : 0 ≤ c) (hgrad : ∀ (w : E), s < dist w x → dist w x < r → c ≤ ‖gradient f w‖) (hzs : dist z x ≤ s) (hfz : f z < f x + c * (r - s)) {t : ℝ} (ht : 0 ≤ t) : dist (φ.toFun t z) x ≤ r

An energy barrier confines stable trajectories. Suppose that ‖∇ f‖ ≥ c on the open annulus s < dist w x < r. A trajectory of a negative gradient flow converging to x that starts within distance s of x at a value below f x + c * (r - s) never leaves the closed ball of radius r about x: to cross the annulus it would have to lose at least c * (r - s) of f, more than it has to spare above its limiting value.

theorem Flow.IsNegativeGradient.dist_le_of_mem_unstableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} {x z : E} (hφ : φ.IsNegativeGradient f) (hz : z ∈ φ.unstableSet x) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (φ.toFun t z)) (hfx : ContinuousAt f x) {s r c : ℝ} (hc : 0 ≤ c) (hgrad : ∀ (w : E), s < dist w x → dist w x < r → c ≤ ‖gradient f w‖) (hzs : dist z x ≤ s) (hfz : f x - c * (r - s) < f z) {t : ℝ} (ht : t ≤ 0) : dist (φ.toFun t z) x ≤ r

An energy barrier confines unstable trajectories. The backward-time counterpart of Flow.IsNegativeGradient.dist_le_of_mem_stableSet: if ‖∇ f‖ ≥ c on the open annulus s < dist w x < r, a trajectory converging to x in backward time that starts within distance s of x at a value above f x - c * (r - s) stays in the closed ball of radius r about x at all nonpositive times.