Breaking of orbits between stable and unstable sets

Let φ be a real flow on a pseudometric space, and let x be a point and r > 0 a radius whose sphere is compact. Assume that every forward orbit trapped in the closed ball of radius r about x converges to x, and so does every trapped backward orbit. Suppose that points u n, infinitely many of which lie outside the stable set W^s(x), converge to a point y of W^s(x). Then the orbits of these u n follow the orbit of y into the ball, linger near x for longer and longer, and must eventually leave it again. Their exit points, reached at times tending to +∞, accumulate at a point of the sphere of radius r lying in the unstable set W^u(x).

This is the mechanism by which a sequence of trajectories converges to a broken trajectory: the limit of the orbits of the u n runs along the orbit of y into x and leaves x along an orbit of W^u(x). Iterating it at the successive rest points is the core of the compactness theorem for spaces of Morse trajectories. The trapping hypotheses are stated for an arbitrary flow; for a negative gradient flow they follow from the absence of other critical points in the ball (TauCeti.Analysis.Calculus.Morse.Breaking).

Main declarations

• Flow.exists_tendsto_mem_unstableSet_of_tendsto_mem_stableSet: exit points of the orbits of the u n, taken at times tending to +∞, converge to a point of W^u(x) at distance r from x.
• Flow.exists_tendsto_mem_stableSet_of_tendsto_mem_unstableSet: the time-reversed statement.
• Flow.exists_mem_closure_inter_unstableSet_of_mem_closure_inter_stableSet and Flow.exists_mem_closure_inter_stableSet_of_mem_closure_inter_unstableSet: the closure of an invariant set disjoint from W^s(x) (respectively W^u(x)) that meets W^s(x) (respectively W^u(x)) also meets W^u(x) (respectively W^s(x)) on the sphere of radius r.

References

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

theorem Flow.exists_tendsto_mem_unstableSet_of_tendsto_mem_stableSet {α : Type u_1} [PseudoMetricSpace α] {φ : Flow ℝ α} {x : α} {r : ℝ} (hr : 0 < r) (hcompact : IsCompact (Metric.sphere x r)) (hfwd : ∀ (w : α), (∀ (t : ℝ), 0 ≤ t → φ.toFun t w ∈ Metric.closedBall x r) → w ∈ φ.stableSet x) (hbwd : ∀ (w : α), (∀ t ≤ 0, φ.toFun t w ∈ Metric.closedBall x r) → w ∈ φ.unstableSet x) {y : α} (hy : y ∈ φ.stableSet x) {u : ℕ → α} (hu : Filter.Tendsto u Filter.atTop (nhds y)) (hux : ∃ᶠ (n : ℕ) in Filter.atTop, u n ∉ φ.stableSet x) : ∃ z ∈ φ.unstableSet x, dist z x = r ∧ ∃ (n : ℕ → ℕ) (t : ℕ → ℝ), Filter.Tendsto n Filter.atTop Filter.atTop ∧ Filter.Tendsto t Filter.atTop Filter.atTop ∧ Filter.Tendsto (fun (k : ℕ) => φ.toFun (t k) (u (n k))) Filter.atTop (nhds z)

Orbits break between stable and unstable sets. Let r > 0 have a compact sphere about x. Assume that every forward orbit trapped in closedBall x r converges to x in forward time, and every trapped backward orbit converges to x in backward time. If points u n, frequently outside the stable set of x, converge to a point y of that stable set, then along a sequence of indices n k → ∞ and of times t k → +∞ the points φ (t k) (u (n k)) converge to a point z of the unstable set of x at distance exactly r from x.

The backward trapping hypothesis ensures that the limit z converges to x in backward time. Only the sphere needs to be compact; the ambient space need not be proper.

theorem Flow.exists_tendsto_mem_stableSet_of_tendsto_mem_unstableSet {α : Type u_1} [PseudoMetricSpace α] {φ : Flow ℝ α} {x : α} {r : ℝ} (hr : 0 < r) (hcompact : IsCompact (Metric.sphere x r)) (hfwd : ∀ (w : α), (∀ (t : ℝ), 0 ≤ t → φ.toFun t w ∈ Metric.closedBall x r) → w ∈ φ.stableSet x) (hbwd : ∀ (w : α), (∀ t ≤ 0, φ.toFun t w ∈ Metric.closedBall x r) → w ∈ φ.unstableSet x) {y : α} (hy : y ∈ φ.unstableSet x) {u : ℕ → α} (hu : Filter.Tendsto u Filter.atTop (nhds y)) (hux : ∃ᶠ (n : ℕ) in Filter.atTop, u n ∉ φ.unstableSet x) : ∃ z ∈ φ.stableSet x, dist z x = r ∧ ∃ (n : ℕ → ℕ) (t : ℕ → ℝ), Filter.Tendsto n Filter.atTop Filter.atTop ∧ Filter.Tendsto t Filter.atTop Filter.atBot ∧ Filter.Tendsto (fun (k : ℕ) => φ.toFun (t k) (u (n k))) Filter.atTop (nhds z)

Orbits break between unstable and stable sets. The time reversal of Flow.exists_tendsto_mem_unstableSet_of_tendsto_mem_stableSet: if points u n, frequently outside the unstable set of x, converge to a point of it, then along indices n k → ∞ and times t k → -∞ the points φ (t k) (u (n k)) converge to a point of the stable set of x at distance r from x.

theorem Flow.exists_mem_closure_inter_unstableSet_of_mem_closure_inter_stableSet {α : Type u_1} [PseudoMetricSpace α] {φ : Flow ℝ α} {x : α} {r : ℝ} (hr : 0 < r) (hcompact : IsCompact (Metric.sphere x r)) (hfwd : ∀ (w : α), (∀ (t : ℝ), 0 ≤ t → φ.toFun t w ∈ Metric.closedBall x r) → w ∈ φ.stableSet x) (hbwd : ∀ (w : α), (∀ t ≤ 0, φ.toFun t w ∈ Metric.closedBall x r) → w ∈ φ.unstableSet x) {S : Set α} (hS : IsInvariant φ.toFun S) (hSx : Disjoint S (φ.stableSet x)) {y : α} (hy : y ∈ closure S ∩ φ.stableSet x) : ∃ z ∈ closure S ∩ φ.unstableSet x, dist z x = r

The closure of an invariant set continues from a stable to an unstable set. If an invariant set S is disjoint from the stable set of x but its closure meets that stable set, then its closure also meets the unstable set of x, at distance exactly r from x, for every radius r with compact sphere and the forward and backward trapping properties.

theorem Flow.exists_mem_closure_inter_stableSet_of_mem_closure_inter_unstableSet {α : Type u_1} [PseudoMetricSpace α] {φ : Flow ℝ α} {x : α} {r : ℝ} (hr : 0 < r) (hcompact : IsCompact (Metric.sphere x r)) (hfwd : ∀ (w : α), (∀ (t : ℝ), 0 ≤ t → φ.toFun t w ∈ Metric.closedBall x r) → w ∈ φ.stableSet x) (hbwd : ∀ (w : α), (∀ t ≤ 0, φ.toFun t w ∈ Metric.closedBall x r) → w ∈ φ.unstableSet x) {S : Set α} (hS : IsInvariant φ.toFun S) (hSx : Disjoint S (φ.unstableSet x)) {y : α} (hy : y ∈ closure S ∩ φ.unstableSet x) : ∃ z ∈ closure S ∩ φ.stableSet x, dist z x = r

The closure of an invariant set continues from an unstable to a stable set. The time reversal of Flow.exists_mem_closure_inter_unstableSet_of_mem_closure_inter_stableSet.