ω-limits

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 atTop, 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 omegaLimit locale provides the localised notation ω for omegaLimit, as well as ω⁺ and ω⁻ for omegaLimit atTop and omegaLimit atBot respectively for when the acting monoid is endowed with an order.

Definition and notation

def omegaLimit {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) : Set β

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

def omegaLimit.termω : Lean.ParserDescr

def omegaLimit.«termω⁺» : Lean.ParserDescr

def omegaLimit.«termω⁻» : Lean.ParserDescr

Elementary properties

theorem omegaLimit_def {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) : omegaLimit f ϕ s = ⋂ (u : Set τ) (_ : u ∈ f), closure (Set.image2 ϕ u s)

theorem omegaLimit_subset_of_tendsto {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (ϕ : τ → α → β) (s : Set α) {m : τ → τ} {f₁ : Filter τ} {f₂ : Filter τ} (hf : Filter.Tendsto m f₁ f₂) : omegaLimit f₁ (fun t x => ϕ (m t) x) s ⊆ omegaLimit f₂ ϕ s

theorem omegaLimit_mono_left {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (ϕ : τ → α → β) (s : Set α) {f₁ : Filter τ} {f₂ : Filter τ} (hf : f₁ ≤ f₂) : omegaLimit f₁ ϕ s ⊆ omegaLimit f₂ ϕ s

theorem omegaLimit_mono_right {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) {s₁ : Set α} {s₂ : Set α} (hs : s₁ ⊆ s₂) : omegaLimit f ϕ s₁ ⊆ omegaLimit f ϕ s₂

theorem isClosed_omegaLimit {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) : IsClosed (omegaLimit f ϕ s)

theorem mapsTo_omegaLimit' {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (s : Set α) {α' : Type u_5} {β' : Type u_6} [TopologicalSpace β'] {f : Filter τ} {ϕ : τ → α → β} {ϕ' : τ → α' → β'} {ga : α → α'} {s' : Set α'} (hs : Set.MapsTo ga s s') {gb : β → β'} (hg : ∀ᶠ (t : τ) in f, Set.EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s) (hgc : Continuous gb) : Set.MapsTo gb (omegaLimit f ϕ s) (omegaLimit f ϕ' s')

theorem mapsTo_omegaLimit {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (s : Set α) {α' : Type u_5} {β' : Type u_6} [TopologicalSpace β'] {f : Filter τ} {ϕ : τ → α → β} {ϕ' : τ → α' → β'} {ga : α → α'} {s' : Set α'} (hs : Set.MapsTo ga s s') {gb : β → β'} (hg : ∀ (t : τ) (x : α), gb (ϕ t x) = ϕ' t (ga x)) (hgc : Continuous gb) : Set.MapsTo gb (omegaLimit f ϕ s) (omegaLimit f ϕ' s')

theorem omegaLimit_image_eq {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (s : Set α) {α' : Type u_5} (ϕ : τ → α' → β) (f : Filter τ) (g : α → α') : omegaLimit f ϕ (g '' s) = omegaLimit f (fun t x => ϕ t (g x)) s

theorem omegaLimit_preimage_subset {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] {α' : Type u_5} (ϕ : τ → α' → β) (s : Set α') (f : Filter τ) (g : α → α') : omegaLimit f (fun t x => ϕ t (g x)) (g ⁻¹' s) ⊆ omegaLimit f ϕ s

Equivalent definitions of the omega limit

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

theorem mem_omegaLimit_iff_frequently {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) (y : β) : y ∈ omegaLimit f ϕ s ↔ ∀ (n : Set β), n ∈ nhds y → ∃ᶠ (t : τ) in f, Set.Nonempty (s ∩ ϕ t ⁻¹' n)

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_omegaLimit_iff_frequently₂ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) (y : β) : y ∈ omegaLimit f ϕ s ↔ ∀ (n : Set β), n ∈ nhds y → ∃ᶠ (t : τ) in f, Set.Nonempty (ϕ t '' s ∩ n)

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_omegaLimit_singleton_iff_map_cluster_point {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (x : α) (y : β) : y ∈ omegaLimit f ϕ {x} ↔ MapClusterPt y f fun 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 omegaLimit_inter {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s₁ : Set α) (s₂ : Set α) : omegaLimit f ϕ (s₁ ∩ s₂) ⊆ omegaLimit f ϕ s₁ ∩ omegaLimit f ϕ s₂

theorem omegaLimit_iInter {τ : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_4} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (p : ι → Set α) : omegaLimit f ϕ (⋂ (i : ι), p i) ⊆ ⋂ (i : ι), omegaLimit f ϕ (p i)

theorem omegaLimit_union {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s₁ : Set α) (s₂ : Set α) : omegaLimit f ϕ (s₁ ∪ s₂) = omegaLimit f ϕ s₁ ∪ omegaLimit f ϕ s₂

theorem omegaLimit_iUnion {τ : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_4} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (p : ι → Set α) : ⋃ (i : ι), omegaLimit f ϕ (p i) ⊆ omegaLimit 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 omegaLimit_eq_iInter {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) : omegaLimit f ϕ s = ⋂ (u : ↑f.sets), closure (Set.image2 ϕ (↑u) s)

theorem omegaLimit_eq_biInter_inter {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) {v : Set τ} (hv : v ∈ f) : omegaLimit f ϕ s = ⋂ (u : Set τ) (_ : u ∈ f), closure (Set.image2 ϕ (u ∩ v) s)

theorem omegaLimit_eq_iInter_inter {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) {v : Set τ} (hv : v ∈ f) : omegaLimit f ϕ s = ⋂ (u : ↑f.sets), closure (Set.image2 ϕ (↑u ∩ v) s)

theorem omegaLimit_subset_closure_fw_image {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) {u : Set τ} (hu : u ∈ f) : omegaLimit f ϕ s ⊆ closure (Set.image2 ϕ u s)

ω-limits and compactness

theorem eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset' {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) {c : Set β} (hc₁ : IsCompact c) (hc₂ : ∃ v, v ∈ f ∧ closure (Set.image2 ϕ v s) ⊆ c) {n : Set β} (hn₁ : IsOpen n) (hn₂ : omegaLimit f ϕ s ⊆ n) : ∃ u, 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_isCompact_absorbing_of_isOpen_of_omegaLimit_subset {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) [T2Space β] {c : Set β} (hc₁ : IsCompact c) (hc₂ : ∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s c) {n : Set β} (hn₁ : IsOpen n) (hn₂ : omegaLimit f ϕ s ⊆ n) : ∃ u, 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_mapsTo_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) [T2Space β] {c : Set β} (hc₁ : IsCompact c) (hc₂ : ∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s c) {n : Set β} (hn₁ : IsOpen n) (hn₂ : omegaLimit f ϕ s ⊆ n) : ∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s n

theorem eventually_closure_subset_of_isOpen_of_omegaLimit_subset {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) [CompactSpace β] {v : Set β} (hv₁ : IsOpen v) (hv₂ : omegaLimit f ϕ s ⊆ v) : ∃ u, u ∈ f ∧ closure (Set.image2 ϕ u s) ⊆ v

theorem eventually_mapsTo_of_isOpen_of_omegaLimit_subset {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) [CompactSpace β] {v : Set β} (hv₁ : IsOpen v) (hv₂ : omegaLimit f ϕ s ⊆ v) : ∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s v

theorem nonempty_omegaLimit_of_isCompact_absorbing {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) [Filter.NeBot f] {c : Set β} (hc₁ : IsCompact c) (hc₂ : ∃ v, v ∈ f ∧ closure (Set.image2 ϕ v s) ⊆ c) (hs : Set.Nonempty s) : Set.Nonempty (omegaLimit f ϕ s)

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

theorem nonempty_omegaLimit {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) [CompactSpace β] [Filter.NeBot f] (hs : Set.Nonempty s) : Set.Nonempty (omegaLimit f ϕ s)

ω-limits of Flows by a Monoid

theorem Flow.isInvariant_omegaLimit {τ : Type u_1} [TopologicalSpace τ] [AddMonoid τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (f : Filter τ) (ϕ : Flow τ α) (s : Set α) (hf : ∀ (t : τ), Filter.Tendsto ((fun x x_1 => x + x_1) t) f f) : IsInvariant ϕ.toFun (omegaLimit f ϕ.toFun s)

theorem Flow.omegaLimit_image_subset {τ : Type u_1} [TopologicalSpace τ] [AddMonoid τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (f : Filter τ) (ϕ : Flow τ α) (s : Set α) (t : τ) (ht : Filter.Tendsto (fun x => x + t) f f) : omegaLimit f ϕ.toFun (Flow.toFun ϕ t '' s) ⊆ omegaLimit f ϕ.toFun s

ω-limits of Flows by a Group

@[simp]

theorem Flow.omegaLimit_image_eq {τ : Type u_1} [TopologicalSpace τ] [AddCommGroup τ] [TopologicalAddGroup τ] {α : Type u_2} [TopologicalSpace α] (f : Filter τ) (ϕ : Flow τ α) (s : Set α) (hf : ∀ (t : τ), Filter.Tendsto (fun x => x + t) f f) (t : τ) : omegaLimit f ϕ.toFun (Flow.toFun ϕ t '' s) = omegaLimit f ϕ.toFun s

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

theorem Flow.omegaLimit_omegaLimit {τ : Type u_1} [TopologicalSpace τ] [AddCommGroup τ] [TopologicalAddGroup τ] {α : Type u_2} [TopologicalSpace α] (f : Filter τ) (ϕ : Flow τ α) (s : Set α) (hf : ∀ (t : τ), Filter.Tendsto ((fun x x_1 => x + x_1) t) f f) : omegaLimit f ϕ.toFun (omegaLimit f ϕ.toFun s) ⊆ omegaLimit f ϕ.toFun s