mathlib3 documentation

dynamics.omega_limit

ω-limits #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

For a function ϕ : τ → α → β where β is a topological space, we define the ω-limit under ϕ of a set s in α with respect to filter f on τ: an element y : β is in the ω-limit of s if the forward images of s intersect arbitrarily small neighbourhoods of y frequently "in the direction of f".

In practice ϕ is often a continuous monoid-act, but the definition requires only that ϕ has a coercion to the appropriate function type. In the case where τ is ℕ or ℝ and f is at_top, we recover the usual definition of the ω-limit set as the set of all y such that there exist sequences (tₙ), (xₙ) such that ϕ tₙ xₙ ⟶ y as n ⟶ ∞.

Notations #

The omega_limit locale provides the localised notation ω for omega_limit, as well as ω⁺ and ω⁻ for omega_limit at_top and omega_limit at_bot respectively for when the acting monoid is endowed with an order.

Definition and notation #

def omega_limit {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s : set α) :

set β

The ω-limit of a set s under ϕ with respect to a filter f is ⋂ u ∈ f, cl (ϕ u s).

Equations

omega_limit f ϕ s = ⋂ (u : set τ) (H : u ∈ f), closure (set.image2 ϕ u s)

Elementary properties #

theorem omega_limit_def {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s : set α) :

omega_limit f ϕ s = ⋂ (u : set τ) (H : u ∈ f), closure (set.image2 ϕ u s)

theorem omega_limit_subset_of_tendsto {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (ϕ : τ → α → β) (s : set α) {m : τ → τ} {f₁ f₂ : filter τ} (hf : filter.tendsto m f₁ f₂) :

omega_limit f₁ (λ (t : τ) (x : α), ϕ (m t) x) s ⊆ omega_limit f₂ ϕ s

theorem omega_limit_mono_left {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (ϕ : τ → α → β) (s : set α) {f₁ f₂ : filter τ} (hf : f₁ ≤ f₂) :

omega_limit f₁ ϕ s ⊆ omega_limit f₂ ϕ s

theorem omega_limit_mono_right {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) {s₁ s₂ : set α} (hs : s₁ ⊆ s₂) :

omega_limit f ϕ s₁ ⊆ omega_limit f ϕ s₂

theorem is_closed_omega_limit {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s : set α) :

is_closed (omega_limit f ϕ s)

theorem maps_to_omega_limit' {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (s : set α) {α' : Type u_4} {β' : Type u_5} [topological_space β'] {f : filter τ} {ϕ : τ → α → β} {ϕ' : τ → α' → β'} {ga : α → α'} {s' : set α'} (hs : set.maps_to ga s s') {gb : β → β'} (hg : ∀ᶠ (t : τ) in f, set.eq_on (gb ∘ ϕ t) (ϕ' t ∘ ga) s) (hgc : continuous gb) :

set.maps_to gb (omega_limit f ϕ s) (omega_limit f ϕ' s')

theorem maps_to_omega_limit {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (s : set α) {α' : Type u_4} {β' : Type u_5} [topological_space β'] {f : filter τ} {ϕ : τ → α → β} {ϕ' : τ → α' → β'} {ga : α → α'} {s' : set α'} (hs : set.maps_to ga s s') {gb : β → β'} (hg : ∀ (t : τ) (x : α), gb (ϕ t x) = ϕ' t (ga x)) (hgc : continuous gb) :

set.maps_to gb (omega_limit f ϕ s) (omega_limit f ϕ' s')

theorem omega_limit_image_eq {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (s : set α) {α' : Type u_4} (ϕ : τ → α' → β) (f : filter τ) (g : α → α') :

omega_limit f ϕ (g '' s) = omega_limit f (λ (t : τ) (x : α), ϕ t (g x)) s

theorem omega_limit_preimage_subset {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] {α' : Type u_4} (ϕ : τ → α' → β) (s : set α') (f : filter τ) (g : α → α') :

omega_limit f (λ (t : τ) (x : α), ϕ t (g x)) (g ⁻¹' s) ⊆ omega_limit f ϕ s

Equivalent definitions of the omega limit #

The next few lemmas are various versions of the property characterising ω-limits:

theorem mem_omega_limit_iff_frequently {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s : set α) (y : β) :

y ∈ omega_limit f ϕ s ↔ ∀ (n : set β), n ∈ nhds y → (∃ᶠ (t : τ) in f, (s ∩ ϕ t ⁻¹' n).nonempty)

An element y is in the ω-limit set of s w.r.t. f if the preimages of an arbitrary neighbourhood of y frequently (w.r.t. f) intersects of s.

theorem mem_omega_limit_iff_frequently₂ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s : set α) (y : β) :

y ∈ omega_limit f ϕ s ↔ ∀ (n : set β), n ∈ nhds y → (∃ᶠ (t : τ) in f, (ϕ t '' s ∩ n).nonempty)

An element y is in the ω-limit set of s w.r.t. f if the forward images of s frequently (w.r.t. f) intersect arbitrary neighbourhoods of y.

theorem mem_omega_limit_singleton_iff_map_cluster_point {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (x : α) (y : β) :

y ∈ omega_limit f ϕ {x} ↔ map_cluster_pt y f (λ (t : τ), ϕ t x)

An element y is in the ω-limit of x w.r.t. f if the forward images of x frequently (w.r.t. f) falls within an arbitrary neighbourhood of y.

Set operations and omega limits #

theorem omega_limit_inter {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s₁ s₂ : set α) :

omega_limit f ϕ (s₁ ∩ s₂) ⊆ omega_limit f ϕ s₁ ∩ omega_limit f ϕ s₂

theorem omega_limit_Inter {τ : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_4} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (p : ι → set α) :

omega_limit f ϕ (⋂ (i : ι), p i) ⊆ ⋂ (i : ι), omega_limit f ϕ (p i)

theorem omega_limit_union {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s₁ s₂ : set α) :

omega_limit f ϕ (s₁ ∪ s₂) = omega_limit f ϕ s₁ ∪ omega_limit f ϕ s₂

theorem omega_limit_Union {τ : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_4} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (p : ι → set α) :

(⋃ (i : ι), omega_limit f ϕ (p i)) ⊆ omega_limit f ϕ (⋃ (i : ι), p i)

Different expressions for omega limits, useful for rewrites. In particular, one may restrict the intersection to sets in f which are subsets of some set v also in f.

theorem omega_limit_eq_Inter {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s : set α) :

omega_limit f ϕ s = ⋂ (u : ↥(f.sets)), closure (set.image2 ϕ ↑u s)

theorem omega_limit_eq_bInter_inter {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s : set α) {v : set τ} (hv : v ∈ f) :

omega_limit f ϕ s = ⋂ (u : set τ) (H : u ∈ f), closure (set.image2 ϕ (u ∩ v) s)

theorem omega_limit_eq_Inter_inter {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s : set α) {v : set τ} (hv : v ∈ f) :

omega_limit f ϕ s = ⋂ (u : ↥(f.sets)), closure (set.image2 ϕ (↑u ∩ v) s)

theorem omega_limit_subset_closure_fw_image {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s : set α) {u : set τ} (hu : u ∈ f) :

omega_limit f ϕ s ⊆ closure (set.image2 ϕ u s)

`ω-limits and compactness #

theorem eventually_closure_subset_of_is_compact_absorbing_of_is_open_of_omega_limit_subset' {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s : set α) {c : set β} (hc₁ : is_compact c) (hc₂ : ∃ (v : set τ) (H : v ∈ f), closure (set.image2 ϕ v s) ⊆ c) {n : set β} (hn₁ : is_open n) (hn₂ : omega_limit f ϕ s ⊆ n) :

∃ (u : set τ) (H : u ∈ f), closure (set.image2 ϕ u s) ⊆ n

A set is eventually carried into any open neighbourhood of its ω-limit: if c is a compact set such that closure {ϕ t x | t ∈ v, x ∈ s} ⊆ c for some v ∈ f and n is an open neighbourhood of ω f ϕ s, then for some u ∈ f we have closure {ϕ t x | t ∈ u, x ∈ s} ⊆ n.

theorem eventually_closure_subset_of_is_compact_absorbing_of_is_open_of_omega_limit_subset {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s : set α) [t2_space β] {c : set β} (hc₁ : is_compact c) (hc₂ : ∀ᶠ (t : τ) in f, set.maps_to (ϕ t) s c) {n : set β} (hn₁ : is_open n) (hn₂ : omega_limit f ϕ s ⊆ n) :

∃ (u : set τ) (H : u ∈ f), closure (set.image2 ϕ u s) ⊆ n

A set is eventually carried into any open neighbourhood of its ω-limit: if c is a compact set such that closure {ϕ t x | t ∈ v, x ∈ s} ⊆ c for some v ∈ f and n is an open neighbourhood of ω f ϕ s, then for some u ∈ f we have closure {ϕ t x | t ∈ u, x ∈ s} ⊆ n.

theorem eventually_maps_to_of_is_compact_absorbing_of_is_open_of_omega_limit_subset {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s : set α) [t2_space β] {c : set β} (hc₁ : is_compact c) (hc₂ : ∀ᶠ (t : τ) in f, set.maps_to (ϕ t) s c) {n : set β} (hn₁ : is_open n) (hn₂ : omega_limit f ϕ s ⊆ n) :

∀ᶠ (t : τ) in f, set.maps_to (ϕ t) s n

theorem eventually_closure_subset_of_is_open_of_omega_limit_subset {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s : set α) [compact_space β] {v : set β} (hv₁ : is_open v) (hv₂ : omega_limit f ϕ s ⊆ v) :

∃ (u : set τ) (H : u ∈ f), closure (set.image2 ϕ u s) ⊆ v

theorem eventually_maps_to_of_is_open_of_omega_limit_subset {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s : set α) [compact_space β] {v : set β} (hv₁ : is_open v) (hv₂ : omega_limit f ϕ s ⊆ v) :

∀ᶠ (t : τ) in f, set.maps_to (ϕ t) s v

theorem nonempty_omega_limit_of_is_compact_absorbing {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s : set α) [f.ne_bot] {c : set β} (hc₁ : is_compact c) (hc₂ : ∃ (v : set τ) (H : v ∈ f), closure (set.image2 ϕ v s) ⊆ c) (hs : s.nonempty) :

(omega_limit f ϕ s).nonempty

The ω-limit of a nonempty set w.r.t. a nontrivial filter is nonempty.

theorem nonempty_omega_limit {τ : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space β] (f : filter τ) (ϕ : τ → α → β) (s : set α) [compact_space β] [f.ne_bot] (hs : s.nonempty) :

(omega_limit f ϕ s).nonempty

ω-limits of Flows by a Monoid #

theorem flow.is_invariant_omega_limit {τ : Type u_1} [topological_space τ] [add_monoid τ] [has_continuous_add τ] {α : Type u_2} [topological_space α] (f : filter τ) (ϕ : flow τ α) (s : set α) (hf : ∀ (t : τ), filter.tendsto (has_add.add t) f f) :

is_invariant ⇑ϕ (omega_limit f ⇑ϕ s)

theorem flow.omega_limit_image_subset {τ : Type u_1} [topological_space τ] [add_monoid τ] [has_continuous_add τ] {α : Type u_2} [topological_space α] (f : filter τ) (ϕ : flow τ α) (s : set α) (t : τ) (ht : filter.tendsto (λ (_x : τ), _x + t) f f) :

omega_limit f ⇑ϕ (⇑ϕ t '' s) ⊆ omega_limit f ⇑ϕ s

ω-limits of Flows by a Group #

@[simp]

theorem flow.omega_limit_image_eq {τ : Type u_1} [topological_space τ] [add_comm_group τ] [topological_add_group τ] {α : Type u_2} [topological_space α] (f : filter τ) (ϕ : flow τ α) (s : set α) (hf : ∀ (t : τ), filter.tendsto (λ (_x : τ), _x + t) f f) (t : τ) :

omega_limit f ⇑ϕ (⇑ϕ t '' s) = omega_limit f ⇑ϕ s

the ω-limit of a forward image of s is the same as the ω-limit of s.

theorem flow.omega_limit_omega_limit {τ : Type u_1} [topological_space τ] [add_comm_group τ] [topological_add_group τ] {α : Type u_2} [topological_space α] (f : filter τ) (ϕ : flow τ α) (s : set α) (hf : ∀ (t : τ), filter.tendsto (has_add.add t) f f) :

omega_limit f ⇑ϕ (omega_limit f ⇑ϕ s) ⊆ omega_limit f ⇑ϕ s