The Morse–Smale condition for a negative-gradient flow

Let E be a real Hilbert space and f : E → ℝ a function whose gradient is globally Lipschitz, so that the negative-gradient flow negativeGradientFlow f hf exists for all time. The results on transverse intersections and level slices of connecting trajectories (TauCeti.Analysis.Calculus.Morse.Transversality, …TrajectorySpace) take transversality of the unstable set of p and the stable set of q at a point y as a hypothesis. The predicate and its elementary API need only completeness of E; the consequences drawn from it assume E finite-dimensional.

IsMorseSmale f hf states that this transversality holds at every common point of the unstable set of every nondegenerate critical point p and the stable set of every nondegenerate critical point q. It is the global transversality hypothesis htr : IsMorseSmale f hf of the results on breaking of trajectories, compactness of trajectory spaces and the mod-two Morse boundary. For a Morse function (all of whose critical points are nondegenerate), this is the classical Morse–Smale condition. It is a plain predicate: the regularity of f is a separate hypothesis of the statements that use it.

Main declarations

• TauCeti.IsMorseSmale f hf: the unstable set of each nondegenerate critical point p and the stable set of each nondegenerate critical point q are transverse at each of their common points.
• TauCeti.IsMorseSmale.of_forall and TauCeti.IsMorseSmale.transverse_at: its introduction and pointwise elimination rules.
• TauCeti.isMorseSmale_congr: the predicate does not depend on the Lipschitz witness.
• TauCeti.IsMorseSmale.of_forall_exists_negativeGradientFlow: for a C² function it suffices to check transversality at one point of each connecting trajectory.
• TauCeti.IsMorseSmale.morseIndex_lt: for a Morse–Smale function, a trajectory between two different nondegenerate critical points runs from higher to strictly lower Morse index.
• TauCeti.IsMorseSmale.unstableSet_inter_stableSet_eq_empty: consequently no trajectory runs from p to a different nondegenerate critical point q with morseIndex f p ≤ morseIndex f q.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 2 (the Morse–Smale condition).

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

The Morse–Smale condition. For a function f with K-Lipschitz gradient, the unstable set of each nondegenerate critical point p and the stable set of each nondegenerate critical point q of the negative-gradient flow are transverse at each common point y: the spans of their tangent cones at y together span the whole space. (When E is finite-dimensional and f is C², these sets are C¹ manifolds near y, by the slice charts IsNondegenerateCriticalPoint.exists_unstableSet_chart and …exists_stableSet_chart, and these spans are their tangent spaces.)

theorem TauCeti.IsMorseSmale.of_forall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {K : NNReal} {hf : LipschitzWith K (gradient f)} (h : ∀ ⦃p q y : E⦄, IsNondegenerateCriticalPoint f p → IsNondegenerateCriticalPoint f q → y ∈ (negativeGradientFlow f hf).unstableSet p ∩ (negativeGradientFlow f hf).stableSet q → Submodule.span ℝ (tangentConeAt ℝ ((negativeGradientFlow f hf).unstableSet p) y) ⊔ Submodule.span ℝ (tangentConeAt ℝ ((negativeGradientFlow f hf).stableSet q) y) = ⊤) : IsMorseSmale f hf

The introduction rule for IsMorseSmale. A function is Morse–Smale once, at every point y of W^u(p) ∩ W^s(q) for nondegenerate critical points p and q, the spans of the tangent cones of the unstable set of p and the stable set of q together span the whole space.

theorem TauCeti.IsMorseSmale.transverse_at {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {K : NNReal} {hf : LipschitzWith K (gradient f)} (h : IsMorseSmale f hf) {p q y : E} (hp : IsNondegenerateCriticalPoint f p) (hq : IsNondegenerateCriticalPoint f q) (hy : y ∈ (negativeGradientFlow f hf).unstableSet p ∩ (negativeGradientFlow f hf).stableSet q) : Submodule.span ℝ (tangentConeAt ℝ ((negativeGradientFlow f hf).unstableSet p) y) ⊔ Submodule.span ℝ (tangentConeAt ℝ ((negativeGradientFlow f hf).stableSet q) y) = ⊤

The pointwise elimination rule for IsMorseSmale. For a Morse–Smale function, at a point y of W^u(p) ∩ W^s(q), for nondegenerate critical points p and q, the spans of the tangent cones of the unstable set of p and the stable set of q together span the whole space.

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

Independence of the Lipschitz witness. The Morse–Smale condition does not depend on the Lipschitz bound used to define the negative-gradient flow.

theorem TauCeti.IsMorseSmale.of_forall_exists_negativeGradientFlow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {K : NNReal} {hf : LipschitzWith K (gradient f)} (hfs : ContDiff ℝ 2 f) (h : ∀ ⦃p q y : E⦄, IsNondegenerateCriticalPoint f p → IsNondegenerateCriticalPoint f q → y ∈ (negativeGradientFlow f hf).unstableSet p ∩ (negativeGradientFlow f hf).stableSet q → ∃ (t : ℝ), Submodule.span ℝ (tangentConeAt ℝ ((negativeGradientFlow f hf).unstableSet p) ((negativeGradientFlow f hf).toFun t y)) ⊔ Submodule.span ℝ (tangentConeAt ℝ ((negativeGradientFlow f hf).stableSet q) ((negativeGradientFlow f hf).toFun t y)) = ⊤) : IsMorseSmale f hf

One point per trajectory suffices. For a C² function, the Morse–Smale condition holds as soon as, on the trajectory through each point y of W^u(p) ∩ W^s(q), the unstable set of p and the stable set of q are transverse at some point φ_t y: transversality propagates along trajectories.

theorem TauCeti.IsMorseSmale.morseIndex_lt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {f : E → ℝ} {K : NNReal} {hf : LipschitzWith K (gradient f)} {p q y : E} (h : IsMorseSmale f hf) (hp : IsNondegenerateCriticalPoint f p) (hq : IsNondegenerateCriticalPoint f q) (hfs : ContDiff ℝ 2 f) (hpq : p ≠ q) (hyu : y ∈ (negativeGradientFlow f hf).unstableSet p) (hys : y ∈ (negativeGradientFlow f hf).stableSet q) : morseIndex f q < morseIndex f p

The Morse index drops along trajectories. For a C² Morse–Smale function, a trajectory of the negative-gradient flow from a nondegenerate critical point p to a different nondegenerate critical point q forces morseIndex f q < morseIndex f p.

theorem TauCeti.IsMorseSmale.unstableSet_inter_stableSet_eq_empty {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {f : E → ℝ} {K : NNReal} {hf : LipschitzWith K (gradient f)} {p q : E} (h : IsMorseSmale f hf) (hp : IsNondegenerateCriticalPoint f p) (hq : IsNondegenerateCriticalPoint f q) (hfs : ContDiff ℝ 2 f) (hpq : p ≠ q) (hind : morseIndex f p ≤ morseIndex f q) : (negativeGradientFlow f hf).unstableSet p ∩ (negativeGradientFlow f hf).stableSet q = ∅

No trajectories up the index. For a C² Morse–Smale function, the unstable set of a nondegenerate critical point p does not meet the stable set of a different nondegenerate critical point q whose Morse index is at least that of p.