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.

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}.