Stable and unstable sets of a flow

For a real flow φ, the stable set of x consists of the points whose trajectories converge to x as time tends to +∞; the unstable set uses time tending to -∞. These are the underlying sets which the stable-manifold theorem identifies locally as smooth manifolds near a hyperbolic fixed point.

Both sets are invariant under the entire flow. Moreover, either set can be nonempty only when its limiting point is fixed by the flow. Time reversal exchanges the two constructions.

Main declarations

• Flow.stableSet: points converging to a given point in forward time.
• Flow.unstableSet: points converging to a given point in backward time.
• Flow.isInvariant_stableSet and Flow.isInvariant_unstableSet: invariance under time translation.
• Flow.fixed_of_mem_stableSet and Flow.fixed_of_mem_unstableSet: a limiting point of a trajectory is fixed.
• Flow.stableSet_reverse and Flow.unstableSet_reverse: time reversal exchanges stable and unstable sets.
• Homeomorph.image_stableSet_eq and Homeomorph.image_unstableSet_eq: a topological conjugacy transports stable and unstable sets.

References

The stable and unstable set viewpoint follows M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext (2014), Chapter 2, §2.1.d. The conjugacy and coordinate-transport perspective is used throughout D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS (2012), Chapters 2–4 and 10, with analytic background in Appendices A–C.

def Flow.stableSet {α : Type u_1} [TopologicalSpace α] (φ : Flow ℝ α) (x : α) : Set α

The stable set of x under a real flow φ: the points whose trajectories converge to x as time tends to +∞.

Equations

• φ.stableSet x = {y : α | Filter.Tendsto (fun (t : ℝ) => φ.toFun t y) Filter.atTop (nhds x)}

def Flow.unstableSet {α : Type u_1} [TopologicalSpace α] (φ : Flow ℝ α) (x : α) : Set α

The unstable set of x under a real flow φ: the points whose trajectories converge to x as time tends to -∞.

Equations

• φ.unstableSet x = {y : α | Filter.Tendsto (fun (t : ℝ) => φ.toFun t y) Filter.atBot (nhds x)}

@[simp]

theorem Flow.mem_stableSet {α : Type u_1} [TopologicalSpace α] {φ : Flow ℝ α} {x y : α} : y ∈ φ.stableSet x ↔ Filter.Tendsto (fun (t : ℝ) => φ.toFun t y) Filter.atTop (nhds x)

Membership in a stable set means convergence of the trajectory in forward time.

@[simp]

theorem Flow.mem_unstableSet {α : Type u_1} [TopologicalSpace α] {φ : Flow ℝ α} {x y : α} : y ∈ φ.unstableSet x ↔ Filter.Tendsto (fun (t : ℝ) => φ.toFun t y) Filter.atBot (nhds x)

Membership in an unstable set means convergence of the trajectory in backward time.

theorem Flow.isInvariant_stableSet {α : Type u_1} [TopologicalSpace α] (φ : Flow ℝ α) (x : α) : IsInvariant φ.toFun (φ.stableSet x)

The stable set of a point is invariant under every time map of the flow.

theorem Flow.isInvariant_unstableSet {α : Type u_1} [TopologicalSpace α] (φ : Flow ℝ α) (x : α) : IsInvariant φ.toFun (φ.unstableSet x)

The unstable set of a point is invariant under every time map of the flow.

theorem Flow.fixed_of_mem_stableSet {α : Type u_1} [TopologicalSpace α] [T2Space α] {φ : Flow ℝ α} {x y : α} (hy : y ∈ φ.stableSet x) (t : ℝ) : φ.toFun t x = x

If some trajectory converges to x in forward time, then x is fixed by every time map of the flow.

theorem Flow.fixed_of_mem_unstableSet {α : Type u_1} [TopologicalSpace α] [T2Space α] {φ : Flow ℝ α} {x y : α} (hy : y ∈ φ.unstableSet x) (t : ℝ) : φ.toFun t x = x

If some trajectory converges to x in backward time, then x is fixed by every time map of the flow.

@[simp]

theorem Flow.self_mem_stableSet_iff {α : Type u_1} [TopologicalSpace α] [T2Space α] {φ : Flow ℝ α} {x : α} : x ∈ φ.stableSet x ↔ ∀ (t : ℝ), φ.toFun t x = x

A point belongs to its stable set exactly when it is fixed by the flow.

@[simp]

theorem Flow.self_mem_unstableSet_iff {α : Type u_1} [TopologicalSpace α] [T2Space α] {φ : Flow ℝ α} {x : α} : x ∈ φ.unstableSet x ↔ ∀ (t : ℝ), φ.toFun t x = x

A point belongs to its unstable set exactly when it is fixed by the flow.

@[simp]

theorem Flow.reverse_reverse {α : Type u_1} [TopologicalSpace α] {τ : Type u_2} [TopologicalSpace τ] [SubtractionCommMonoid τ] [ContinuousNeg τ] (φ : Flow τ α) : φ.reverse.reverse = φ

Time reversal is an involution.

@[simp]

theorem Flow.stableSet_reverse {α : Type u_1} [TopologicalSpace α] (φ : Flow ℝ α) (x : α) : φ.reverse.stableSet x = φ.unstableSet x

Time reversal exchanges stable and unstable sets.

@[simp]

theorem Flow.unstableSet_reverse {α : Type u_1} [TopologicalSpace α] (φ : Flow ℝ α) (x : α) : φ.reverse.unstableSet x = φ.stableSet x

Time reversal exchanges unstable and stable sets.

@[simp]

theorem Flow.stableSet_id {α : Type u_1} [TopologicalSpace α] [T1Space α] (x : α) : (Flow.id ℝ α).stableSet x = {x}

Under the identity flow, the stable set of x is the singleton {x}.

@[simp]

theorem Flow.unstableSet_id {α : Type u_1} [TopologicalSpace α] [T1Space α] (x : α) : (Flow.id ℝ α).unstableSet x = {x}

Under the identity flow, the unstable set of x is the singleton {x}.

theorem Topology.IsInducing.map_mem_stableSet_iff {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] {φ : Flow ℝ α} {ψ : Flow ℝ β} {f : α → β} (hf : IsInducing f) (hconj : Flow.IsSemiconjugacy f φ ψ) {x y : α} : f y ∈ ψ.stableSet (f x) ↔ y ∈ φ.stableSet x

An inducing semiconjugacy carries membership in a stable set to membership in the corresponding stable set.

theorem Homeomorph.map_mem_stableSet_iff {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] {φ : Flow ℝ α} {ψ : Flow ℝ β} (e : α ≃ₜ β) (hconj : Flow.IsSemiconjugacy (⇑e) φ ψ) {x y : α} : e y ∈ ψ.stableSet (e x) ↔ y ∈ φ.stableSet x

A topological conjugacy carries membership in a stable set to membership in the corresponding stable set. This is stated as an explicit rewrite lemma because Flow.mem_stableSet already puts its left-hand side in simp-normal form.

theorem Homeomorph.image_stableSet_eq {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] {φ : Flow ℝ α} {ψ : Flow ℝ β} (e : α ≃ₜ β) (hconj : Flow.IsSemiconjugacy (⇑e) φ ψ) (x : α) : ⇑e '' φ.stableSet x = ψ.stableSet (e x)

A topological conjugacy carries a stable set to the corresponding stable set.

theorem Topology.IsInducing.map_mem_unstableSet_iff {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] {φ : Flow ℝ α} {ψ : Flow ℝ β} {f : α → β} (hf : IsInducing f) (hconj : Flow.IsSemiconjugacy f φ ψ) {x y : α} : f y ∈ ψ.unstableSet (f x) ↔ y ∈ φ.unstableSet x

An inducing semiconjugacy carries membership in an unstable set to membership in the corresponding unstable set. This is stated as an explicit rewrite lemma because Flow.mem_unstableSet already puts its left-hand side in simp-normal form.

theorem Homeomorph.map_mem_unstableSet_iff {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] {φ : Flow ℝ α} {ψ : Flow ℝ β} (e : α ≃ₜ β) (hconj : Flow.IsSemiconjugacy (⇑e) φ ψ) {x y : α} : e y ∈ ψ.unstableSet (e x) ↔ y ∈ φ.unstableSet x

A topological conjugacy carries membership in an unstable set to membership in the corresponding unstable set. This is stated as an explicit rewrite lemma because Flow.mem_unstableSet already puts its left-hand side in simp-normal form.

theorem Homeomorph.image_unstableSet_eq {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] {φ : Flow ℝ α} {ψ : Flow ℝ β} (e : α ≃ₜ β) (hconj : Flow.IsSemiconjugacy (⇑e) φ ψ) (x : α) : ⇑e '' φ.unstableSet x = ψ.unstableSet (e x)

A topological conjugacy carries an unstable set to the corresponding unstable set.

theorem Flow.eq_of_mem_stableSet_of_periodic {α : Type u_1} [TopologicalSpace α] [T1Space α] {φ : Flow ℝ α} {q x : α} (hx : x ∈ φ.stableSet q) {T : ℝ} (hT : T ≠ 0) (hper : Function.Periodic (fun (t : ℝ) => φ.toFun t x) T) : x = q

A periodic flow orbit with a forward limit equals its limit.

theorem Flow.eq_of_mem_unstableSet_of_periodic {α : Type u_1} [TopologicalSpace α] [T1Space α] {φ : Flow ℝ α} {q x : α} (hx : x ∈ φ.unstableSet q) {T : ℝ} (hT : T ≠ 0) (hper : Function.Periodic (fun (t : ℝ) => φ.toFun t x) T) : x = q

A periodic flow orbit with a backward limit equals its limit.

theorem Flow.orbit_injective_of_mem_stableSet_of_ne {α : Type u_1} [TopologicalSpace α] [T1Space α] {φ : Flow ℝ α} {q x : α} (hx : x ∈ φ.stableSet q) (hxq : x ≠ q) : Function.Injective fun (t : ℝ) => φ.toFun t x

A nonconstant orbit that converges in forward time is injectively parametrized by time.

theorem Flow.orbit_injective_of_mem_unstableSet_of_ne {α : Type u_1} [TopologicalSpace α] [T1Space α] {φ : Flow ℝ α} {q x : α} (hx : x ∈ φ.unstableSet q) (hxq : x ≠ q) : Function.Injective fun (t : ℝ) => φ.toFun t x

A nonconstant orbit that converges in backward time is injectively parametrized by time.