eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset
theorem eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset :
∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β)
(s : Set α) [inst_1 : T2Space β] {c : Set β},
IsCompact c →
(∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s c) →
∀ {n : Set β}, IsOpen n → omegaLimit f ϕ s ⊆ n → ∃ u ∈ f, closure (Set.image2 ϕ u s) ⊆ n
This theorem states that if a set is eventually carried into any open neighbourhood of its omega limit, given a compact set `c` such that the closure of the image of a binary function `ϕ` applied to `t` in a set `v` and `x` in a set `s` is a subset of `c` for some `v` in a filter `f`, and `n` is an open neighbourhood of the omega limit of `f`, `ϕ`, and `s`, then there exists some `u` in `f` such that the closure of the image of `ϕ` applied to `t` in `u` and `x` in `s` is a subset of `n`.
In simpler terms, this theorem says that if we have a compact set that absorbs the eventual behavior of a dynamic system (described by the function `ϕ`), then any open neighbourhood of the long term behavior (omega limit) of this system also absorbs the system for some point onwards (i.e., for some `u` in the filter `f`).
More concisely: If a compact set contains the eventual images of a function under a filter, then there exists a set in the filter whose images under the function are contained in any open neighborhood of the omega limit.
|
nonempty_omegaLimit_of_isCompact_absorbing
theorem nonempty_omegaLimit_of_isCompact_absorbing :
∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β)
(s : Set α) [inst_1 : f.NeBot] {c : Set β},
IsCompact c → (∃ v ∈ f, closure (Set.image2 ϕ v s) ⊆ c) → s.Nonempty → (omegaLimit f ϕ s).Nonempty
This theorem states that the omega-limit of a nonempty set with respect to a nontrivial filter is also nonempty. Specifically, given a topological space `β`, a filter `f` on some type `τ`, a map `ϕ` from `τ` and another type `α` into `β`, and a set `s` of type `α`, if the filter is nontrivial, and there exists a compact set `c` in `β` such that the closure of the image of the set `s` under the map `ϕ` and some element of the filter is a subset of `c`, then the omega-limit of the set `s` under the map `ϕ` with respect to the filter `f` is nonempty.
More concisely: If `β` is a topological space, `f` is a nontrivial filter on a type `τ`, `ϕ:` `τ` → `β`, `s` is a nonempty set of type `α`, and there exists a compact set `c` in `β` such that the closure of `ϕ[s]` intersects some element of `f`, then the omega-limit of `s` under `ϕ` with respect to `f` is nonempty.
|
mem_omegaLimit_iff_frequently
theorem mem_omegaLimit_iff_frequently :
∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β)
(s : Set α) (y : β), y ∈ omegaLimit f ϕ s ↔ ∀ n ∈ nhds y, ∃ᶠ (t : τ) in f, (s ∩ ϕ t ⁻¹' n).Nonempty
The theorem `mem_omegaLimit_iff_frequently` states that for any types `τ`, `α`, and `β`, where `β` has a topological space structure, a filter `f` on `τ`, a function `ϕ` from `τ` to `α` to `β`, a set `s` of type `α`, and an element `y` of type `β`, the element `y` belongs to the ω-limit of the set `s` under the function `ϕ` with respect to the filter `f` if and only if for any neighborhood `n` of `y`, there exist frequently (with respect to `f`) times `t` such that the set `s` intersects the preimage of `n` under `ϕ t`. The preimage of a set `n` under `ϕ t` refers to all elements in `α` that `ϕ t` maps into `n`. The neighborhood `n` of `y` refers to the set of points in a topological space that are near `y`. The term "frequently" here refers to the occurrence of an event in the context of a filter, which loosely corresponds to the event happening "often" or "for most elements".
More concisely: For any filter `f` on type `τ`, function `ϕ` from `τ` to a topological space `β`, set `s` of type `α`, and element `y` of `β`, `y` is in the ω-limit of `s` under `ϕ` with respect to `f` if and only if for every neighborhood `n` of `y`, there exist infinitely many times `t` such that `s` intersects the preimage of `n` under `ϕ t`.
|
Flow.omegaLimit_image_eq
theorem Flow.omegaLimit_image_eq :
∀ {τ : Type u_1} [inst : TopologicalSpace τ] [inst_1 : AddCommGroup τ] [inst_2 : TopologicalAddGroup τ]
{α : Type u_2} [inst_3 : TopologicalSpace α] (f : Filter τ) (ϕ : Flow τ α) (s : Set α),
(∀ (t : τ), Filter.Tendsto (fun x => x + t) f f) →
∀ (t : τ), omegaLimit f ϕ.toFun (ϕ.toFun t '' s) = omegaLimit f ϕ.toFun s
The theorem `Flow.omegaLimit_image_eq` states that for any topological spaces `τ` and `α`, where `τ` is also an additive commutative group with a compatible topology, given a filter `f` on `τ`, a flow `ϕ` on `τ` to `α`, and a set `s` in `α`, if the function `(fun x => x + t)` tends to `f` for every `t` in `τ`, then the ω-limit of the image of `s` under the function `ϕ.toFun t` is equal to the ω-limit of `s` itself. In simpler terms, the ω-limit of the future states of a set `s` under a flow is the same as the ω-limit of the set `s` itself. This is a fundamental property in the study of dynamical systems.
More concisely: For any topological space `τ` that is an additive commutative group with a compatible topology, filter `f` on `τ`, set `s` in `α`, and flow `ϕ` from `τ` to `α`, if `(x ↦ x + t)` converges to `f` for all `t` in `τ`, then the ω-limit of `s` under `ϕ.toFun` is equal to the ω-limit of `s`.
|
mem_omegaLimit_iff_frequently₂
theorem mem_omegaLimit_iff_frequently₂ :
∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β)
(s : Set α) (y : β), y ∈ omegaLimit f ϕ s ↔ ∀ n ∈ nhds y, ∃ᶠ (t : τ) in f, (ϕ t '' s ∩ n).Nonempty
The theorem `mem_omegaLimit_iff_frequently₂` states that an element `y` is in the ω-limit set of a set `s` with respect to a filter `f` if and only if for every neighborhood `n` of `y`, there exists frequently (with respect to `f`) a time `t` such that the forward image of `s` at time `t` intersects with `n`. Here, the forward image of `s` at time `t` is obtained by applying the function `ϕ` at time `t` to each element of `s`, and a neighborhood of `y` is a set containing an open set around `y`.
More concisely: An element is in the ω-limit set of a set with respect to a filter if and only if for every neighborhood of the element, there exists a time frequently reached under the filter such that the forward image of the set at that time intersects the neighborhood.
|
omegaLimit_subset_of_tendsto
theorem omegaLimit_subset_of_tendsto :
∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (ϕ : τ → α → β) (s : Set α) {m : τ → τ}
{f₁ f₂ : Filter τ}, Filter.Tendsto m f₁ f₂ → omegaLimit f₁ (fun t x => ϕ (m t) x) s ⊆ omegaLimit f₂ ϕ s
The theorem `omegaLimit_subset_of_tendsto` states that for any types `τ`, `α`, and `β` with `β` having a topological space structure, along with a function `ϕ : τ → α → β`, a set `s` of type `α`, a function `m : τ → τ`, and two filters `f₁` and `f₂` on `τ`, if `m` tends towards `f₂` with respect to filter `f₁` (denoted by `Filter.Tendsto m f₁ f₂`), then the ω-limit of set `s` under the function `(fun t x => ϕ (m t) x)` with respect to filter `f₁` is a subset of the ω-limit of set `s` under function `ϕ` with respect to filter `f₂`. In other words, if we transform the time scale of a dynamical system using a function that tends to a limit under a certain filter, the ω-limit set of the transformed system is contained in the ω-limit set of the original system under the limit filter.
More concisely: If a function `ϕ : τ -> α -> β` maps the ω-limit of a set `s` in `α` under filter `f₁` to a subset of its ω-limit under filter `f₂`, when `m : τ -> τ` tends towards `f₂` with respect to filter `f₁`.
|
Mathlib.Dynamics.OmegaLimit._auxLemma.4
theorem Mathlib.Dynamics.OmegaLimit._auxLemma.4 :
∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β)
(s : Set α) (y : β), (y ∈ omegaLimit f ϕ s) = ∀ n ∈ nhds y, ∃ᶠ (t : τ) in f, (s ∩ ϕ t ⁻¹' n).Nonempty
This theorem, `Mathlib.Dynamics.OmegaLimit._auxLemma.4`, states that for any types `τ`, `α`, `β`, and assuming `β` is a topological space, for any filter `f` on `τ`, a function `ϕ` from `τ` to `α` to `β`, a set `s` of type `α`, and a point `y` of type `β`, `y` is in the ω-limit of the set `s` under the function `ϕ` with respect to the filter `f` if and only if for every neighborhood `n` of `y`, there eventually exists `t` in the filter `f` such that the set `s` intersects the pre-image of the neighborhood `n` through the function `ϕ(t)` is not empty. Here, "eventually exists" is quantified in the sense of the filter `f`, and a set is non-empty if there exists an element that belongs to the set.
More concisely: A point `y` in a topological space is in the ω-limit of a set `s` under a function `ϕ` with respect to a filter `f` if and only if for every neighborhood `n` of `y`, there exists a filter element `t` such that `s` intersects the pre-image of `n` under `ϕ(t)` is non-empty.
|
mem_omegaLimit_singleton_iff_map_cluster_point
theorem mem_omegaLimit_singleton_iff_map_cluster_point :
∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (x : α)
(y : β), y ∈ omegaLimit f ϕ {x} ↔ MapClusterPt y f fun t => ϕ t x
The theorem `mem_omegaLimit_singleton_iff_map_cluster_point` states that for any topological space `β`, any filter `f` on a type `τ`, and any function `ϕ` from `τ` and `α` to `β`, for any elements `x` of type `α` and `y` of type `β`, `y` belongs to the ω-limit of the singleton set `{x}` with respect to `f` and `ϕ` if and only if `y` is a map-cluster point of `f` under the function `t => ϕ t x`. In other words, `y` is in the ω-limit of `x` under `f` if the images of `x` under `ϕ` frequently (with respect to `f`) fall within any neighborhood of `y`.
More concisely: The ω-limit of a singleton set {x} with respect to a filter f and a function ϕ is equal to the set of map-cluster points of f under the function t => ϕ(t, x).
|
eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset'
theorem eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset' :
∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β)
(s : Set α) {c : Set β},
IsCompact c →
(∃ v ∈ f, closure (Set.image2 ϕ v s) ⊆ c) →
∀ {n : Set β}, IsOpen n → omegaLimit f ϕ s ⊆ n → ∃ u ∈ f, closure (Set.image2 ϕ u s) ⊆ n
This theorem states that if we have a compact set `c` and a set `s`, under some transformation `ϕ` with respect to a filter `f`, such that the closure of the image of the set `s` under the transformation `ϕ` for any `t` in some `v` in `f` is a subset of `c`, then for any open neighbourhood `n` of the omega-limit of the set `s` under the transformation `ϕ` with respect to the filter `f`, there exists some `u` in `f` such that the closure of the image of the set `s` under the transformation `ϕ` for any `t` in `u` is a subset of `n`. This essentially means that the set is eventually carried into any open neighbourhood of its omega-limit.
More concisely: If a compact set `c` contains the closure of the image of any set `s` under transformation `ϕ` for all `t` in some filter `f` element `v`, then for any open neighborhood `n` of the omega-limit of `s` under `ϕ` with respect to `f`, there exists some `u` in `f` such that the image of `s` under `ϕ` for all `t` in `u` is contained in `n`.
|
omegaLimit_mono_right
theorem omegaLimit_mono_right :
∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β)
{s₁ s₂ : Set α}, s₁ ⊆ s₂ → omegaLimit f ϕ s₁ ⊆ omegaLimit f ϕ s₂
The `omegaLimit_mono_right` theorem states that for any types `τ`, `α` and `β` where `β` possesses a topology, any filter `f` over `τ`, and any function `ϕ` mapping from `τ × α` to `β`, if we have two sets `s₁` and `s₂` of type `α` such that `s₁` is a subset of `s₂`, then the ω-limit of `s₁` under `ϕ` with respect to filter `f` is also a subset of the ω-limit of `s₂` under `ϕ` with respect to the same filter `f`. In other words, if an input set is a subset of another, their respective ω-limits follow the same subset relation.
More concisely: If `s₁ ⊆ s₂` are subsets of `α`, then the ω-limit of `s₁` under a function `ϕ` with respect to filter `f` over `τ` is a subset of the ω-limit of `s₂` under the same function and filter.
|