Negative gradient trajectories break at nondegenerate critical points

A negative gradient trajectory trapped, in forward time, in a closed ball containing no critical point other than its centre x converges to x; the same holds in backward time. So the radius of such a ball satisfies the trapping hypotheses of TauCeti.Dynamics.Flow.Breaking, and every sufficiently small radius about a nondegenerate critical point does.

Feeding this into Flow.exists_tendsto_mem_unstableSet_of_tendsto_mem_stableSet gives the elementary step of the compactness theorem for spaces of Morse trajectories. If trajectories converging to a critical point q accumulate on a trajectory converging instead to a nondegenerate critical point x ≠ q, then they also accumulate on a nonconstant trajectory leaving x: the limit is a trajectory broken at x. In terms of sets, the closure of the stable set W^s(q) meets the unstable set W^u(x) on every small sphere about x. The time-reversed statement holds for unstable sets.

Main declarations

• Flow.IsNegativeGradient.mem_stableSet_of_forall_mem_closedBall and Flow.IsNegativeGradient.mem_unstableSet_of_forall_mem_closedBall: a trajectory trapped in a closed ball whose only critical point is its centre converges to the centre.
• TauCeti.IsNondegenerateCriticalPoint.eventually_forall_mem_stableSet_of_forall_mem_closedBall and its unstable counterpart: every small radius about a nondegenerate critical point isolates it.
• TauCeti.IsNondegenerateCriticalPoint.eventually_exists_mem_closure_stableSet_inter_unstableSet and its time reversal TauCeti.IsNondegenerateCriticalPoint.eventually_exists_mem_closure_unstableSet_inter_stableSet: limits of trajectories break at a nondegenerate critical point.
• TauCeti.IsNondegenerateCriticalPoint.exists_isChain_of_mem_closure_stableSet_inter_stableSet and its time reversal: finite chains of nonconstant connecting orbits, with length bounded by the index drop.
• TauCeti.IsNondegenerateCriticalPoint.morseIndex_lt_of_mem_closure_stableSet_inter_stableSet and its time reversal: iterating breaks through convergent Morse--Smale trajectories strictly lowers the Morse index.
• TauCeti.IsMorseSmale.isClosed_unstableSet_inter_stableSet_inter_level and TauCeti.IsNondegenerateCriticalPoint.finite_unstableSet_inter_stableSet_inter_level: an index-one trajectory slice is closed, and is finite when it is contained in a compact set.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 3 (compactness of spaces of trajectories).

theorem Flow.IsNegativeGradient.mem_stableSet_of_forall_mem_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {φ : Flow ℝ E} {f : E → ℝ} {x : E} {r : ℝ} (hφ : φ.IsNegativeGradient f) (hdiff : ∀ y ∈ Metric.closedBall x r, DifferentiableAt ℝ f y) (hgrad : ContinuousOn (gradient f) (Metric.closedBall x r)) (hcrit : ∀ y ∈ Metric.closedBall x r, gradient f y = 0 → y = x) {w : E} (hw : ∀ (t : ℝ), 0 ≤ t → φ.toFun t w ∈ Metric.closedBall x r) : w ∈ φ.stableSet x

A trajectory trapped near an isolated critical point converges to it. If f is differentiable with continuous gradient on closedBall x r, and x is the only critical point of f in that ball, then a negative gradient trajectory staying in the ball at all nonnegative times converges to x.

theorem Flow.IsNegativeGradient.mem_unstableSet_of_forall_mem_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {φ : Flow ℝ E} {f : E → ℝ} {x : E} {r : ℝ} (hφ : φ.IsNegativeGradient f) (hdiff : ∀ y ∈ Metric.closedBall x r, DifferentiableAt ℝ f y) (hgrad : ContinuousOn (gradient f) (Metric.closedBall x r)) (hcrit : ∀ y ∈ Metric.closedBall x r, gradient f y = 0 → y = x) {w : E} (hw : ∀ t ≤ 0, φ.toFun t w ∈ Metric.closedBall x r) : w ∈ φ.unstableSet x

A trajectory trapped near an isolated critical point converges to it in backward time. The backward-time counterpart of Flow.IsNegativeGradient.mem_stableSet_of_forall_mem_closedBall.

theorem TauCeti.IsNondegenerateCriticalPoint.eventually_forall_mem_stableSet_of_forall_mem_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {φ : Flow ℝ E} {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) (hφ : φ.IsNegativeGradient f) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (w : E), (∀ (t : ℝ), 0 ≤ t → φ.toFun t w ∈ Metric.closedBall x r) → w ∈ φ.stableSet x

Small balls isolate a nondegenerate critical point in forward time. For every sufficiently small r > 0, a negative gradient trajectory staying in closedBall x r at all nonnegative times converges to the nondegenerate critical point x.

theorem TauCeti.IsNondegenerateCriticalPoint.eventually_forall_mem_unstableSet_of_forall_mem_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {φ : Flow ℝ E} {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) (hφ : φ.IsNegativeGradient f) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (w : E), (∀ t ≤ 0, φ.toFun t w ∈ Metric.closedBall x r) → w ∈ φ.unstableSet x

Small balls isolate a nondegenerate critical point in backward time. For every sufficiently small r > 0, a negative gradient trajectory staying in closedBall x r at all nonpositive times converges to the nondegenerate critical point x in backward time.

theorem TauCeti.IsNondegenerateCriticalPoint.eventually_exists_mem_closure_stableSet_inter_unstableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {φ : Flow ℝ E} {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) (hφ : φ.IsNegativeGradient f) {q : E} (hqx : q ≠ x) {y : E} (hy : y ∈ closure (φ.stableSet q) ∩ φ.stableSet x) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∃ z ∈ closure (φ.stableSet q) ∩ φ.unstableSet x, dist z x = r

Limits of trajectories break at a nondegenerate critical point. Let x be a nondegenerate critical point and q ≠ x. If a point y of the stable set of x is a limit of points of the stable set of q, then for every sufficiently small r > 0 some point at distance r from x lies both in the unstable set of x and in the closure of the stable set of q.

theorem TauCeti.IsNondegenerateCriticalPoint.eventually_exists_mem_closure_unstableSet_inter_stableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {φ : Flow ℝ E} {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) (hφ : φ.IsNegativeGradient f) {p : E} (hpx : p ≠ x) {y : E} (hy : y ∈ closure (φ.unstableSet p) ∩ φ.unstableSet x) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∃ z ∈ closure (φ.unstableSet p) ∩ φ.stableSet x, dist z x = r

Limits of trajectories break at a nondegenerate critical point, in backward time. Let x be a nondegenerate critical point and p ≠ x. If a point y of the unstable set of x is a limit of points of the unstable set of p, then for every sufficiently small r > 0 some point at distance r from x lies both in the stable set of x and in the closure of the unstable set of p.

Morse-index control along broken limits

theorem TauCeti.IsNondegenerateCriticalPoint.exists_isChain_of_mem_closure_stableSet_inter_stableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} {K : NNReal} {q : E} (hx : IsNondegenerateCriticalPoint f x) (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) (hqx : q ≠ x) (hy : (closure ((negativeGradientFlow f hf).stableSet q) ∩ (negativeGradientFlow f hf).stableSet x).Nonempty) (hconv : ∀ {z : E}, z ∈ closure ((negativeGradientFlow f hf).stableSet q) → ∃ (a : E), IsNondegenerateCriticalPoint f a ∧ z ∈ (negativeGradientFlow f hf).stableSet a) (htr : IsMorseSmale f hf) : ∃ (l : List E), List.IsChain (fun (a b : E) => a ≠ b ∧ ((negativeGradientFlow f hf).unstableSet a ∩ (negativeGradientFlow f hf).stableSet b).Nonempty) (x :: l) ∧ (x :: l).getLast ⋯ = q ∧ (∀ a ∈ x :: l, IsNondegenerateCriticalPoint f a) ∧ l.length + morseIndex f q ≤ morseIndex f x

Suppose every point in the closure of Wˢ(q) converges forward to a nondegenerate critical point, and connecting stable and unstable manifolds meet transversally. If that closure meets Wˢ(x) for x ≠ q, then x :: l is a finite chain from x to q of nondegenerate critical points. Each consecutive pair a ≠ b has a connecting orbit in Wᵘ(a) ∩ Wˢ(b), and the number of components l.length is at most morseIndex f x - morseIndex f q.

theorem TauCeti.IsNondegenerateCriticalPoint.morseIndex_lt_of_mem_closure_stableSet_inter_stableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} {K : NNReal} {q : E} (hx : IsNondegenerateCriticalPoint f x) (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) (hqx : q ≠ x) (hy : (closure ((negativeGradientFlow f hf).stableSet q) ∩ (negativeGradientFlow f hf).stableSet x).Nonempty) (hconv : ∀ {z : E}, z ∈ closure ((negativeGradientFlow f hf).stableSet q) → ∃ (a : E), IsNondegenerateCriticalPoint f a ∧ z ∈ (negativeGradientFlow f hf).stableSet a) (htr : IsMorseSmale f hf) : morseIndex f q < morseIndex f x

Morse index drops along a broken forward limit. Suppose every point in the closure of Wˢ(q) converges forward to a nondegenerate critical point, and all connecting stable and unstable manifolds meet transversally. If that closure meets Wˢ(x) for x ≠ q, then the Morse index of q is strictly smaller than that of x.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_isChain_of_mem_closure_unstableSet_inter_unstableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} {K : NNReal} {p : E} (hx : IsNondegenerateCriticalPoint f x) (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) (hpx : p ≠ x) (hy : (closure ((negativeGradientFlow f hf).unstableSet p) ∩ (negativeGradientFlow f hf).unstableSet x).Nonempty) (hconv : ∀ {z : E}, z ∈ closure ((negativeGradientFlow f hf).unstableSet p) → ∃ (a : E), IsNondegenerateCriticalPoint f a ∧ z ∈ (negativeGradientFlow f hf).unstableSet a) (htr : IsMorseSmale f hf) : ∃ (l : List E), List.IsChain (fun (a b : E) => a ≠ b ∧ ((negativeGradientFlow f hf).unstableSet a ∩ (negativeGradientFlow f hf).stableSet b).Nonempty) (p :: l) ∧ (p :: l).getLast ⋯ = x ∧ (∀ a ∈ p :: l, IsNondegenerateCriticalPoint f a) ∧ l.length + morseIndex f x ≤ morseIndex f p

Suppose every point in the closure of Wᵘ(p) converges backward to a nondegenerate critical point, and connecting stable and unstable manifolds meet transversally. If that closure meets Wᵘ(x) for x ≠ p, then p :: l is a finite chain from p to x of nondegenerate critical points. Each consecutive pair a ≠ b has a connecting orbit in Wᵘ(a) ∩ Wˢ(b), and l.length is at most morseIndex f p - morseIndex f x.

theorem TauCeti.IsNondegenerateCriticalPoint.morseIndex_lt_of_mem_closure_unstableSet_inter_unstableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} {K : NNReal} {p : E} (hx : IsNondegenerateCriticalPoint f x) (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) (hpx : p ≠ x) (hy : (closure ((negativeGradientFlow f hf).unstableSet p) ∩ (negativeGradientFlow f hf).unstableSet x).Nonempty) (hconv : ∀ {z : E}, z ∈ closure ((negativeGradientFlow f hf).unstableSet p) → ∃ (a : E), IsNondegenerateCriticalPoint f a ∧ z ∈ (negativeGradientFlow f hf).unstableSet a) (htr : IsMorseSmale f hf) : morseIndex f x < morseIndex f p

Morse index drops along a broken backward limit. Suppose every point in the closure of Wᵘ(p) converges backward to a nondegenerate critical point, and all connecting stable and unstable manifolds meet transversally. If that closure meets Wᵘ(x) for x ≠ p, then the Morse index of x is strictly smaller than that of p. This is the backward counterpart of morseIndex_lt_of_mem_closure_stableSet_inter_stableSet.

theorem TauCeti.IsMorseSmale.isClosed_unstableSet_inter_stableSet_inter_level {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {K : NNReal} {p q : E} (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) (hind : morseIndex f p = morseIndex f q + 1) {c : ℝ} (hc : f q < c ∧ c < f p) (hconvS : ∀ {z : E}, z ∈ closure ((negativeGradientFlow f hf).stableSet q) → ∃ (b : E), IsNondegenerateCriticalPoint f b ∧ z ∈ (negativeGradientFlow f hf).stableSet b) (hconvU : ∀ {z : E}, z ∈ closure ((negativeGradientFlow f hf).unstableSet p) → ∃ (a : E), IsNondegenerateCriticalPoint f a ∧ z ∈ (negativeGradientFlow f hf).unstableSet a) (htr : IsMorseSmale f hf) : IsClosed ((negativeGradientFlow f hf).unstableSet p ∩ (negativeGradientFlow f hf).stableSet q ∩ {z : E | f z = c})

An index-one Morse trajectory slice is closed. Assume that points in the closures of the relevant stable and unstable manifolds converge to nondegenerate critical points, and that all such manifolds meet transversally. If the Morse indices of p and q differ by one, then their connecting set, cut at any value strictly between f q and f p, is closed.

theorem TauCeti.IsNondegenerateCriticalPoint.finite_unstableSet_inter_stableSet_inter_level {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {K : NNReal} {p q : E} (hp : IsNondegenerateCriticalPoint f p) (hq : IsNondegenerateCriticalPoint f q) (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) (hind : morseIndex f p = morseIndex f q + 1) {c : ℝ} (hc : f q < c ∧ c < f p) (hconvS : ∀ {z : E}, z ∈ closure ((negativeGradientFlow f hf).stableSet q) → ∃ (b : E), IsNondegenerateCriticalPoint f b ∧ z ∈ (negativeGradientFlow f hf).stableSet b) (hconvU : ∀ {z : E}, z ∈ closure ((negativeGradientFlow f hf).unstableSet p) → ∃ (a : E), IsNondegenerateCriticalPoint f a ∧ z ∈ (negativeGradientFlow f hf).unstableSet a) (htr : IsMorseSmale f hf) {C : Set E} (hC : IsCompact C) (hsub : (negativeGradientFlow f hf).unstableSet p ∩ (negativeGradientFlow f hf).stableSet q ∩ {z : E | f z = c} ⊆ C) : ((negativeGradientFlow f hf).unstableSet p ∩ (negativeGradientFlow f hf).stableSet q ∩ {z : E | f z = c}).Finite

A compact index-one Morse trajectory slice is finite. Assume that p and q are nondegenerate critical points and that the hypotheses of IsMorseSmale.isClosed_unstableSet_inter_stableSet_inter_level hold. If the slice is contained in a compact set, then it is finite. This is the finiteness needed to define the coefficient of the Morse differential.