isBounded_le_nhds
theorem isBounded_le_nhds :
∀ {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : BoundedLENhdsClass α] (a : α),
Filter.IsBounded (fun x x_1 => x ≤ x_1) (nhds a)
The theorem `isBounded_le_nhds` states that for any type `α` with a preorder relation and a topological space structure, and assuming that the type `α` belongs to the `BoundedLENhdsClass` class, for any element `a` of type `α`, the neighborhood filter of `a` (denoted by `nhds a`) is eventually bounded with respect to the `≤` relation. In other words, there exists a uniform bound `b` such that eventually every element `x` in the neighborhood of `a` satisfies `x ≤ b`.
More concisely: For any type `α` with a preorder relation and a topological space structure that belongs to `BoundedLENhdsClass`, every element `a` has a uniform bound `b` such that every neighborhood element `x` of `a` satisfies `x ≤ b`.
|
limsSup_eq_of_le_nhds
theorem limsSup_eq_of_le_nhds :
∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] {f : Filter α} {a : α} [inst_3 : f.NeBot], f ≤ nhds a → f.limsSup = a
The theorem `limsSup_eq_of_le_nhds` states that in a conditionally complete linear order equipped with a topological structure that is also an order topology, for any filter `f` that is not an empty Bottom filter, if the filter `f` is less than or equal to the neighborhood filter of a point `a`, then the supremum of all the limits (also known as the limsup) of the filter `f` is equal to `a`. In simpler terms, if a filter is converging towards a particular point, the greatest limit point of the filter coincides with the point the filter is converging to.
More concisely: In a conditionally complete linear order with an order topology, the limsup of a non-empty filter is equal to the filter's infimum in the topology if and only if the filter is contained in the neighborhood filter of its limit point.
|
Filter.Tendsto.liminf_eq
theorem Filter.Tendsto.liminf_eq :
∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] {f : Filter β} {u : β → α} {a : α} [inst_3 : f.NeBot],
Filter.Tendsto u f (nhds a) → Filter.liminf u f = a
This theorem states that for any function `u` from a type `β` to a `ConditionallyCompleteLinearOrder` type `α`, if the function `u` has a limit `a` (in the sense that, for any neighborhood of `a`, the preimage of this neighborhood under `u` is eventually in the filter `f`), then the `liminf` -- the least upper bound of the set of values `a` such that `u(x) ≥ a` eventually holds in the filter `f` -- of `u` along `f` is equal to this limit `a`. Here, it is assumed that `α` is equipped with a topology compatible with its order structure and that `f` is a non-trivial filter.
More concisely: If `u` is a function from type `β` to a conditionally complete linear order `α` with topology compatible with its order structure, and `f` is a non-trivial filter, then `u`'s limit `a` equals the `liminf` of `u` along `f` in `α` if and only if for any neighborhood of `a`, the preimage of that neighborhood under `u` is eventually in `f`.
|
isBounded_ge_nhds
theorem isBounded_ge_nhds :
∀ {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : BoundedGENhdsClass α] (a : α),
Filter.IsBounded (fun x x_1 => x ≥ x_1) (nhds a)
This theorem states that for any type `α` that is a preorder and a topological space, and for any element `a` of type `α`, if `α` is a such that it has a property of being a `BoundedGENhdsClass` (a class of pre-ordered sets that are bounded below in the neighborhood filter), then the filter of neighborhoods around `a` (denoted by `nhds a`) is eventually bounded with respect to the relation `x ≥ x_1`. In other words, for any point `a`, there exists a uniform bound `b` such that in the vicinity of `a` (as defined by the neighborhood filter), all values `x` are greater than or equal to `b`.
More concisely: For any preorder and topological space `α` that is a `BoundedGENhdsClass`, there exists a uniform bound `b` such that for all `a` in `α`, all elements `x` in the neighborhood filter of `a` satisfy `x ≥ b`.
|
liminf_const_sub
theorem liminf_const_sub :
∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
[inst_2 : OrderTopology R] (F : Filter ι) [inst_3 : F.NeBot] [inst_4 : AddCommSemigroup R] [inst_5 : Sub R]
[inst_6 : ContinuousSub R] [inst_7 : OrderedSub R]
[inst_8 : CovariantClass R R (fun x y => x + y) fun x y => x ≤ y] (f : ι → R) (c : R),
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f →
Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F f → Filter.liminf (fun i => c - f i) F = c - Filter.limsup f F
The theorem `liminf_const_sub` states that for any Type `ι`, Type `R` that is a conditionally complete linear order and a topological space with an order topology, any nonempty filter `F` on `ι`, an additive commutative semigroup `R` with subtraction which is continuous and ordered, and a function `f` from `ι` to `R`, if the images of the filter `F` under `f` are eventually bounded above and below, then the limit inferior of the function `(i => c - f i)` along the filter `F` is equal to `c` minus the limit superior of `f` along the filter `F`. Notably, the subtraction operation here is assumed to be associative and transitive under addition, which is expressed by the covariant class constraint.
More concisely: For any nonempty filter on a conditionally complete linear order, if the images of the filter under a continuous, ordered, additive semigroup function are eventually bounded and have limit sup and inf, then the limit inferior of the function difference with a constant is equal to the constant minus the limit superior of the function.
|
eventually_le_limsup
theorem eventually_le_limsup :
∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : FirstCountableTopology α] {f : Filter β} [inst_4 : CountableInterFilter f]
{u : β → α},
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝ → ∀ᶠ (b : β) in f, u b ≤ Filter.limsup u f
The theorem `eventually_le_limsup` states that for any type `α` equipped with a conditionally complete linear order, topological space structure, order topology, and first countable topology, and any type `β`, given a filter `f` for `β` that satisfies the countable intersection property and a function `u` from `β` to `α`, if it is assumed (through `autoParam`) that the image of the filter `f` under `u` is eventually bounded under the less than or equal to relation, then eventually (for `f`), each value `u b` for `b` in `β` is less than or equal to the limit superior (`limsup`) of `u` along `f`. In simpler terms, almost all values of `u` are below the `limsup` in the limit.
Using mathematical notation, it says that if $\{u(b) : b \in \text{Filter } f\}$ is an eventually bounded set, then $\forall b \in \text{Filter } f$, eventually $u(b) \leq \limsup_{b \to f} u(b)$.
More concisely: If a filter on a type equipped with a linear order and topologies satisfies the countable intersection property and its image under a function is eventually bounded, then each element in the filter is eventually less than or equal to the limit superior of the function along that filter.
|
limsup_sub_const
theorem limsup_sub_const :
∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
[inst_2 : OrderTopology R] (F : Filter ι) [inst_3 : F.NeBot] [inst_4 : AddCommSemigroup R] [inst_5 : Sub R]
[inst_6 : ContinuousSub R] [inst_7 : OrderedSub R] (f : ι → R) (c : R),
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f →
Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F f → Filter.limsup (fun i => f i - c) F = Filter.limsup f F - c
The theorem `limsup_sub_const` states that for any given type `ι`, a type `R` which is a conditionally complete linear order with a topological space structure, and for which addition and subtraction are defined and continuously embedded into the order topology, along with a filter `F` on `ι` that is not the bottom element, a function `f : ι → R`, and a constant `c : R`, if the image of `f` under `F` is eventually bounded both above and below (i.e., there exist some uniform upper and lower bounds for the values of `f`), then the limit superior (limsup) of `(f i - c)` over the filter `F` equals the limsup of `f` over `F` minus `c`. In mathematical notation, this is saying that `limsup (f(i) - c) = limsup f(i) - c`.
More concisely: For any conditionally complete linear order `R` with a topological space structure, continuously embedded addition and subtraction, filter `F` on `ι` (without bottom element), function `f : ι → R`, and constant `c : R`, if the image of `f` under `F` is eventually bounded, then `limsup(f(i) - c) = limsup f(i) - c`.
|
liminf_sub_const
theorem liminf_sub_const :
∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
[inst_2 : OrderTopology R] (F : Filter ι) [inst_3 : F.NeBot] [inst_4 : AddCommSemigroup R] [inst_5 : Sub R]
[inst_6 : ContinuousSub R] [inst_7 : OrderedSub R] (f : ι → R) (c : R),
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f →
Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F f → Filter.liminf (fun i => f i - c) F = Filter.liminf f F - c
The theorem `liminf_sub_const` states that for a given filter `F` of type `ι` and a function `f` mapping from `ι` to `R`, where `R` is a conditionally complete linear order with a topological structure, an order topology, an addition commutative semigroup structure, a subtraction operation, a continuous subtraction operation, and an order-preserving subtraction operation, if the image of the filter `F` under the function `f` is eventually bounded from both below and above, then the lower limit (liminf) of the function `f(i) - c` along the filter `F` is equal to the lower limit of the function `f` along the filter `F` minus `c`. In mathematical terms, `liminf (xᵢ - c) = (liminf xᵢ) - c`.
More concisely: For a filter `F` on a conditionally complete linear order `R` with a topological structure, an order topology, an additive commutative semigroup structure, subtraction and continuous order-preserving subtraction operations, if `f: ι → R` has `F`-eventually bounded differences `f(i) - c`, then `liminf (f(i) - c) = liminf f(i) - c`.
|
Antitone.map_limsup_of_continuousAt
theorem Antitone.map_limsup_of_continuousAt :
∀ {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [inst : F.NeBot]
[inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R] [inst_2 : OrderTopology R]
[inst_3 : ConditionallyCompleteLinearOrder S] [inst_4 : TopologicalSpace S] [inst_5 : OrderTopology S]
{f : R → S},
Antitone f →
∀ (a : ι → R),
ContinuousAt f (Filter.limsup a F) →
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F a) _auto✝ →
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F a) _auto✝¹ →
f (Filter.limsup a F) = Filter.liminf (f ∘ a) F
The theorem `Antitone.map_limsup_of_continuousAt` states that for any type `ι`, types `R` and `S` representing conditionally complete linear ordered spaces, and a filter `F` of type `ι`, given a function `f` from `R` to `S` that is antitone and continuous at the `limsup` of a function `a` mapped over the filter `F`, if the filter `F` is bounded from above and below (when mapped under function `a`), then the `limsup` of `a` under `F` when mapped under `f` is equal to the `liminf` of the composition of `f` and `a` under the filter `F`.
In other words, a continuous antitone function sends the least upper bound (limsup) of a filter to the greatest lower bound (liminf) of its images, under the condition that the filter is bounded both from above and below.
More concisely: For antitone and continuous functions `f` between conditionally complete linear ordered spaces `R` and `S`, if `a` is a bounded function from `R` to `S` and `F` is a filter on `R` such that `limsup(a(x))` exists and `f(limsup(a(x))) = liminf(f(a(x)))` for all `x` in `F`, then `limsup(f(a(x)) : S) = liminf(f(a(x)))`.
|
Monotone.map_limsInf_of_continuousAt
theorem Monotone.map_limsInf_of_continuousAt :
∀ {R : Type u_4} {S : Type u_5} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
[inst_2 : OrderTopology R] [inst_3 : ConditionallyCompleteLinearOrder S] [inst_4 : TopologicalSpace S]
[inst_5 : OrderTopology S] {F : Filter R} [inst_6 : F.NeBot] {f : R → S},
Monotone f →
ContinuousAt f F.limsInf →
autoParam (Filter.IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝ →
autoParam (Filter.IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝¹ → f F.limsInf = Filter.liminf f F
The theorem `Monotone.map_limsInf_of_continuousAt` states that for any monotone function `f` mapping between two conditionally complete linear ordered spaces `R` and `S`, if `f` is continuous at the `limsInf` of a specific filter `F` in `R` and `F` is both upper and lower bounded (these are automatic parameters), then the image of the `limsInf` of `F` under `f` equals the `liminf` of the image of `F` under `f`. This illustrates the preservation of liminf under the action of a continuous monotone function.
More concisely: If `f` is a monotone, continuous at the limit of an upper and lower bounded filter in a conditionally complete linear ordered space `R`, then `f` preserves the liminf, that is, `liminf (map f F) = f (limsInf F)`.
|
Monotone.map_liminf_of_continuousAt
theorem Monotone.map_liminf_of_continuousAt :
∀ {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [inst : F.NeBot]
[inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R] [inst_2 : OrderTopology R]
[inst_3 : ConditionallyCompleteLinearOrder S] [inst_4 : TopologicalSpace S] [inst_5 : OrderTopology S]
{f : R → S},
Monotone f →
∀ (a : ι → R),
ContinuousAt f (Filter.liminf a F) →
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F a) _auto✝ →
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F a) _auto✝¹ →
f (Filter.liminf a F) = Filter.liminf (f ∘ a) F
The theorem `Monotone.map_liminf_of_continuousAt` states that for any types `ι`, `R`, and `S`, and any filter `F` on `ι`, given the conditions that `F` is not the bottom filter, `R` and `S` are conditionally complete linear orders equipped with topological spaces and order topologies, and `f` is a monotone function from `R` to `S`. If `a` is a function from `ι` to `R` such that `f` is continuous at the limit inferior (liminf) of `a` with respect to the filter `F`, and it is assumed that the output of `a` under the filter `F` is eventually bounded above and below (captured by the `autoParam` gadgets), then the value of `f` at the liminf of `a` equals the liminf of the function `f ∘ a` (the composition of `f` and `a`) with respect to filter `F`.
In simpler terms, a continuous, monotone function maps the liminf of a sequence to the liminf of the images of the sequence, assuming the sequence is bounded above and below. This applies in the setting of conditionally complete linear ordered spaces.
More concisely: If `F` is a non-bottom filter on `ι`, `R` and `S` are conditionally complete linear orders with topologies, `f` is a monotone and continuous function from `R` to `S`, and `a : ι -> R` has `liminf_F a` bounded, then `f (liminf_F a) = liminf_F (f ∘ a)`.
|
Monotone.map_limsSup_of_continuousAt
theorem Monotone.map_limsSup_of_continuousAt :
∀ {R : Type u_4} {S : Type u_5} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
[inst_2 : OrderTopology R] [inst_3 : ConditionallyCompleteLinearOrder S] [inst_4 : TopologicalSpace S]
[inst_5 : OrderTopology S] {F : Filter R} [inst_6 : F.NeBot] {f : R → S},
Monotone f →
ContinuousAt f F.limsSup →
autoParam (Filter.IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝ →
autoParam (Filter.IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝¹ → f F.limsSup = Filter.limsup f F
This theorem states that for any monotone function `f` that maps from one conditionally complete linear ordered space `R` to another `S`, if `f` is continuous at the least upper bound (`limsSup`) of a filter `F` in `R` and `F` is bounded from above and below, then the value of `f` at the `limsSup` of `F` equals the greatest lower bound (`limsup`) of the image of `F` under `f` in `S`. This theorem involves the concepts of filter theory, topology and order structures in the context of mathematical analysis.
More concisely: If `f` is a monotone, continuous function from the conditionally complete, linearly ordered space `R` to another such space `S`, and `F` is a filter in `R` with a supremum `x` in `R` and an upper bound `y` in `S`, then `f(x) = sup (f(G))`, where `G` is the set of limits of `F`.
|
le_nhds_of_limsSup_eq_limsInf
theorem le_nhds_of_limsSup_eq_limsInf :
∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] {f : Filter α} {a : α},
Filter.IsBounded (fun x x_1 => x ≤ x_1) f →
Filter.IsBounded (fun x x_1 => x ≥ x_1) f → f.limsSup = a → f.limsInf = a → f ≤ nhds a
This theorem states that for any given filter `f` from some type `α`, where `α` is a conditionally complete linear order and also has a topological space structure that is compatible with the linear order (order topology), and for any value `a` from the same type; if `f` is eventually bounded both above and below, and if the least upper bound (limsup) and greatest lower bound (liminf) of `f` are both equal to `a`, then the filter `f` converges to the value `a`. In more formal terms, `f` is less than or equal to the neighborhood filter of `a`.
More concisely: If `α` is a conditionally complete linear order with a compatible topology, `a` is an element of `α`, `f` is a filter on `α` such that `f` is eventually bounded above and below, and `limsup(f) = liminf(f) = a`, then `f` converges to `a`, i.e., `f` is contained in the neighborhood filter of `a`.
|
Filter.Tendsto.limsup_eq
theorem Filter.Tendsto.limsup_eq :
∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] {f : Filter β} {u : β → α} {a : α} [inst_3 : f.NeBot],
Filter.Tendsto u f (nhds a) → Filter.limsup u f = a
This theorem states that for any function `u` from a generic type `β` to a type `α` that is a conditionally complete linear order with a topological structure and order topology, and for any filter `f` on `β` that is not bottom, if `u` tends to a limit `a` as per the neighborhood filter at `a`, then the limit superior (limsup) of `u` along the filter `f` is equal to `a`. In more colloquial terms, if a function has a limit, then its greatest limit (or limit superior) coincides with its actual limit.
More concisely: For any conditionally complete linear order with topology and filter not containing the bottom element, if a function's limit equals its limit superior along the filter, then the function's domain and range have the same limit.
|
Filter.Tendsto.isBoundedUnder_le
theorem Filter.Tendsto.isBoundedUnder_le :
∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : BoundedLENhdsClass α]
{f : Filter ι} {u : ι → α} {a : α},
Filter.Tendsto u f (nhds a) → Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u
The theorem `Filter.Tendsto.isBoundedUnder_le` states that for any types `ι` and `α`, and given a preorder on `α` along with a topological space structure and a proof that `α` is a `BoundedLENhdsClass`, if we have a function `u` from `ι` to `α` and a filter `f` on `ι` such that `u` tends to a specific value `a` in `α` with respect to `f` (meaning, the limit of `u` as `ι` approaches `a` through the filter `f` exists), then it follows that the image of the filter `f` under the function `u` is eventually bounded with respect to the less than or equal to relation. In other words, there exists some bound such that all elements of the image of `f` under `u` are less than or equal to this bound eventually.
More concisely: If `α` is a `BoundedLENhdsClass` with a preorder, `u` is a function from `ι` to `α`, `f` is a filter on `ι`, and `a` is the limit of `u` as `ι` approaches `a` through `f`, then the image of `f` under `u` is eventually bounded by some element in `α` with respect to the less than or equal to relation.
|
tendsto_of_le_liminf_of_limsup_le
theorem tendsto_of_le_liminf_of_limsup_le :
∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] {f : Filter β} {u : β → α} {a : α},
a ≤ Filter.liminf u f →
Filter.limsup u f ≤ a →
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝ →
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝¹ → Filter.Tendsto u f (nhds a)
This theorem states that for any types `α` and `β`, given a conditionally complete linear order on `α`, a topological space structure on `α`, and an order topology on `α`, if you have a filter `f` on `β` and a function `u` from `β` to `α`, and a number `a` of type `α`, then if `a` is less than or equal to the limit inferior (liminf) of `u` at `f` and `a` is greater than or equal to the limit superior (limsup) of `u` at `f`, then `u` tends to `a` along the filter `f`, assuming that the function `u` is eventually bounded both above and below. In mathematical terms, if you have $\liminf_{x\to f} u(x) \leq a \leq \limsup_{x\to f} u(x)$, then $\lim_{x\to f} u(x) = a$.
More concisely: If a conditionally complete linear order on a type `α` has an order topology, and a function from a filter on another type `β` to `α` is eventually bounded both above and below, then the limit of the function along the filter equals the value that is less than or equal to the liminf and greater than or equal to the limsup.
|
liminf_add_const
theorem liminf_add_const :
∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
[inst_2 : OrderTopology R] (F : Filter ι) [inst_3 : F.NeBot] [inst_4 : Add R] [inst_5 : ContinuousAdd R]
[inst_6 : CovariantClass R R (Function.swap fun x y => x + y) fun x y => x ≤ y] (f : ι → R) (c : R),
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f →
Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F f → Filter.liminf (fun i => f i + c) F = Filter.liminf f F + c
This theorem states that for a given filter `F` and a function `f` mapping from type `ι` to a type `R` that is a conditionally complete linear order with a topological space structure, and also supports addition operation which is continuous and covariant, if the image of `F` under `f` is bounded both above (bounded under the less than or equal to relation) and below (bounded under the greater than or equal to relation), then the limit inferior (also known as lower limit) of the function `f` plus a constant `c` with respect to the filter `F` is equal to the limit inferior of the function `f` with respect to the filter `F` plus the constant `c`. This can be expressed in mathematical notation as `liminf (f(i) + c) = liminf f(i) + c`.
More concisely: If `F` is a filter on a conditionally complete linear order `(ι, ≤)` with topological space structure and `f : ι → R` is a continuous, covariant function with respect to `F` such that `⋀i, i ∈ F ⟹ inf(f i) ≤ sup(f i)` holds, then `liminf (f i + c) = liminf (fi) + c`.
|
limsInf_eq_of_le_nhds
theorem limsInf_eq_of_le_nhds :
∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] {f : Filter α} {a : α} [inst_3 : f.NeBot], f ≤ nhds a → f.limsInf = a
This theorem states that for any given type `α`, which is a conditionally complete linear order and a topological space with an order topology, if we have a non-bottom filter `f` on `α` and an element `a` of `α` such that `f` is less than or equal to the neighborhood filter of `a` (which means that `f` converges to `a`), then the limit superior (limsup) of the filter `f` is equal to `a`. This essentially asserts the equivalence between the concepts of a filter converging to a point and its limsup coinciding with that point.
More concisely: For any conditionally complete linear order and topological space `α` with an order topology, if `f` is a non-bottom filter on `α` converging to an element `a`, then `a` is the limsup of `f`.
|
liminf_const_add
theorem liminf_const_add :
∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
[inst_2 : OrderTopology R] (F : Filter ι) [inst_3 : F.NeBot] [inst_4 : Add R] [inst_5 : ContinuousAdd R]
[inst_6 : CovariantClass R R (fun x y => x + y) fun x y => x ≤ y] (f : ι → R) (c : R),
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f →
Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F f → Filter.liminf (fun i => c + f i) F = c + Filter.liminf f F
The theorem `liminf_const_add` states that for a filter `F` on a type `ι` and a function `f` from type `ι` to a conditionally complete linearly ordered topological space `R`, if the function `f` is both eventually bounded above and below with respect to the filter `F`, then the lower limit (or `liminf`) of the function `f` plus a constant `c` with respect to the filter `F` is equal to the constant `c` plus the lower limit of the function `f` with respect to the filter `F`. In mathematical terms, this can be written as `liminf (c + f(i)) = c + liminf f(i)`. This theorem assumes that addition operation is continuous and covariant in the type `R`.
More concisely: For a filter `F` on a type `ι`, a conditionally complete linearly ordered topological space `R` with continuous and covariant addition, and a function `f` from `ι` to `R` that is eventually bounded above and below with respect to `F`, the lower limit of `c + f(i)` equals `c + liminf f(i)`.
|
limsup_const_sub
theorem limsup_const_sub :
∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
[inst_2 : OrderTopology R] (F : Filter ι) [inst_3 : F.NeBot] [inst_4 : AddCommSemigroup R] [inst_5 : Sub R]
[inst_6 : ContinuousSub R] [inst_7 : OrderedSub R]
[inst_8 : CovariantClass R R (fun x y => x + y) fun x y => x ≤ y] (f : ι → R) (c : R),
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f →
Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F f → Filter.limsup (fun i => c - f i) F = c - Filter.liminf f F
This theorem states that for a given type `ι`, a type `R` which is a conditionally complete linear order and a topological space with order topology, and a filter `F` on `ι` that is not equal to the bottom filter (i.e., it is not the empty set), we have the following result for a function `f : ι → R` and a constant `c : R`. If the function `f` is bounded with respect to the order "greater than or equal to" and "less than or equal to" under the filter `F`, then the limit superior (limsup) of the function `(fun i => c - f i)` under the filter `F` is equal to the constant `c` minus the limit inferior (liminf) of `f` under the filter `F`. In mathematical notation, this could be written as `limsup (c - f(i)) = c - liminf f(i)`. This theorem assumes that addition, subtraction, and the order relation in `R` have certain properties, including that subtraction is continuous in the topological space `R`, that `R` has an ordered subtraction operation, and that addition in `R` is covariant (meaning that if `x ≤ y`, then `x + z ≤ y + z`).
More concisely: Given a type `R` with a conditionally complete linear order and order topology, a filter `F` on a type `ι` not equal to the bottom filter, a bounded function `f : ι → R`, and constants `c : R`, the limit superior of `(c - f(i))` under `F` equals `c` minus the limit inferior of `f` under `F`, provided addition, subtraction, and the order relation in `R` have certain properties.
|
tendsto_of_liminf_eq_limsup
theorem tendsto_of_liminf_eq_limsup :
∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] {f : Filter β} {u : β → α} {a : α},
Filter.liminf u f = a →
Filter.limsup u f = a →
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝ →
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝¹ → Filter.Tendsto u f (nhds a)
The theorem `tendsto_of_liminf_eq_limsup` states that for any function `u` from `β` to `α` and any filter `f` on `β`, if the liminf and the limsup of the function `u` with respect to the filter `f` both equal some value `a`, then the function `u` tends to `a` along the filter `f`. Here, `α` is a type with a conditionally complete linear order and a topology that's compatible with the order, `β` is any type, and `a` is a value of type `α`. The function `u` is assumed to be bounded above and below, but these assumptions are provided as an `autoParam`, which means they will be automatically inserted by the Lean prover if not provided.
More concisely: If a function from a filtered space to a conditionally complete ordered topological space has equal liminf and limsup along a filter, then the function converges to that value along the filter.
|
Antitone.map_liminf_of_continuousAt
theorem Antitone.map_liminf_of_continuousAt :
∀ {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [inst : F.NeBot]
[inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R] [inst_2 : OrderTopology R]
[inst_3 : ConditionallyCompleteLinearOrder S] [inst_4 : TopologicalSpace S] [inst_5 : OrderTopology S]
{f : R → S},
Antitone f →
∀ (a : ι → R),
ContinuousAt f (Filter.liminf a F) →
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F a) _auto✝ →
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F a) _auto✝¹ →
f (Filter.liminf a F) = Filter.limsup (f ∘ a) F
This theorem states that, for any type `ι`, real types `R` and `S`, and a filter `F` of type `ι` that is not trivially empty, if `R` and `S` are conditionally complete linearly ordered spaces equipped with their associated topologies and order topologies respectively, then for any antitone function `f: R → S`, for all function `a: ι → R`, if `f` is continuous at the limit inferior (liminf) of `a` with respect to the filter `F`, and if the filter `F` under `a` is eventually bounded both from above and below (where these conditions are automatically provided), then the value of `f` at the liminf of `a` with respect to `F` equals to the limit superior (limsup) of the composition of `f` and `a` with respect to `F`. In short, a continuous antitone function maps the liminf of a function to the limsup of its images, provided that the function's values are eventually bounded both above and below.
More concisely: If `F` is a non-trivial filter on type `ι`, `R` and `S` are conditionally complete linearly ordered spaces with associated topologies, and `f: R → S` is a continuous, antitone function with eventually bounded images under `a: ι → R`, then `f(liminf(a, F)) = limsup(f ∘ a, F)`.
|
tendsto_of_no_upcrossings
theorem tendsto_of_no_upcrossings :
∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderTopology α] [inst_3 : DenselyOrdered α] {f : Filter β} {u : β → α} {s : Set α},
Dense s →
(∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)) →
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝ →
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝¹ → ∃ c, Filter.Tendsto u f (nhds c)
This theorem states that under certain conditions, a sequence must converge. Specifically, let's consider a sequence `u` of elements from a set `β` mapped into a conditionally complete linear order `α` that's also a topological space, and `s` is a dense set of `α`. Suppose `f` is a filter on `β`. The theorem assumes the following:
- For any two distinct elements `a` and `b` from the dense set `s` (with `a < b`), it's not possible for the sequence `u` to be less than `a` and greater than `b` infinitely many times in the filter `f`.
- The sequence `u` is eventually bounded both above and below in the filter `f`.
Under these conditions, there exists an element `c` in `α` such that the sequence `u` converges to `c` in the topology of `α`. This means that for any neighborhood of `c`, there exists a set in the filter `f` such that all elements of the sequence `u` from that set onward are within this neighborhood of `c`.
More concisely: Under the given conditions on a sequence `u` in a conditionally complete linear order `α` that's also a topological space, a dense set `s` in `α`, and a filter `f` on the set `β`, there exists a limit `c` in `α` such that for any neighborhood of `c`, there are infinitely many elements in the sequence `u` from the filter `f` that lie within that neighborhood.
|
Antitone.map_limsInf_of_continuousAt
theorem Antitone.map_limsInf_of_continuousAt :
∀ {R : Type u_4} {S : Type u_5} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
[inst_2 : OrderTopology R] [inst_3 : ConditionallyCompleteLinearOrder S] [inst_4 : TopologicalSpace S]
[inst_5 : OrderTopology S] {F : Filter R} [inst_6 : F.NeBot] {f : R → S},
Antitone f →
ContinuousAt f F.limsInf →
autoParam (Filter.IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝ →
autoParam (Filter.IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝¹ → f F.limsInf = Filter.limsup f F
This theorem states that for any antitone function `f` mapping between two (conditionally) complete linear ordered spaces `R` and `S`, if `f` is continuous at the least upper bound (`limsInf`) of a filter `F` in `R`, and if the filter `F` is bounded both above and below, then the image of the `limsInf` of `F` under `f` is equal to the greatest lower bound (`limsup`) of the image of `F` under `f`. This result holds under the assumptions that `R` and `S` are equipped with topological and order structures that are compatible, that `F` is not a trivial (bottom) filter, and that the boundedness conditions are given as automatic parameters.
More concisely: For any antitone function between two conditionally complete linear ordered spaces with compatible topologies, if the function is continuous at the least upper bound of a bounded above and below filter and the filter is not trivial, then the image of the least upper bound is equal to the greatest lower bound of the function's image under the filter.
|
Monotone.map_limsup_of_continuousAt
theorem Monotone.map_limsup_of_continuousAt :
∀ {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [inst : F.NeBot]
[inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R] [inst_2 : OrderTopology R]
[inst_3 : ConditionallyCompleteLinearOrder S] [inst_4 : TopologicalSpace S] [inst_5 : OrderTopology S]
{f : R → S},
Monotone f →
∀ (a : ι → R),
ContinuousAt f (Filter.limsup a F) →
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F a) _auto✝ →
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F a) _auto✝¹ →
f (Filter.limsup a F) = Filter.limsup (f ∘ a) F
The theorem `Monotone.map_limsup_of_continuousAt` states that for any conditionally complete linear ordered spaces R and S with their respective topologies and order topologies, and for any non-bottom filter F applied to a sequence `a` in R, if `f` is a monotone function from R to S that is continuous at the limit superior (`limsup`) of `a` with respect to the filter F, and the sequence `a` is eventually bounded both below and above (with respect to the filter F), then `f` sends the `limsup` of the sequence `a` to the `limsup` of the images of `a` under `f` with respect to the same filter F.
In mathematical terms, if \( f : R \rightarrow S \) is a continuous, monotone function, and if the sequence \( a : I \rightarrow R \) is eventually bounded from above and below, we have that \( f(\limsup_F(a)) = \limsup_F(f \circ a) \), where \( F \) is a non-trivial filter over an index set \( I \).
More concisely: If `f` is a monotone, continuous function between conditionally complete linear ordered spaces, and a sequence `a` is eventually bounded and `f` is continuous at the limit superior of `a`, then `f` sends the limit superior of `a` to the limit superior of the images of `a` under `f`.
|
limsup_const_add
theorem limsup_const_add :
∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
[inst_2 : OrderTopology R] (F : Filter ι) [inst_3 : F.NeBot] [inst_4 : Add R] [inst_5 : ContinuousAdd R]
[inst_6 : CovariantClass R R (fun x y => x + y) fun x y => x ≤ y] (f : ι → R) (c : R),
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f →
Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F f → Filter.limsup (fun i => c + f i) F = c + Filter.limsup f F
The theorem `limsup_const_add` states that for any type `ι`, a real number type `R` with a conditional complete linear order, a topology, an order topology, an addition operation, a continuous addition, a covariant class for addition and order, a filter `F` on `ι` that is not bottom, a function `f` from `ι` to `R`, and a constant `c` of type `R`, if the image of the filter `F` under `f` is eventually bounded both above and below (in the sense that there are some upper and lower bounds that all the elements eventually do not exceed or fall below respectively), then the supremum limit (limsup) of the function `c + f(i)` along the filter `F` is equal to `c` plus the supremum limit of `f` along the filter `F`. In mathematical terms, it asserts that `limsup (c + f(i)) = c + limsup f(i)`. This theorem essentially describes a property of limit superior in the presence of a constant addition, showing that limsup linearly distributes over addition.
More concisely: For any filter `F` on a type `ι` over a real number type `R` with a conditional complete linear order, if a function `f` from `ι` to `R` has its image under `F` eventually bounded both above and below and `c` is a constant of type `R`, then `limsup (c + f(i)) = c + limsup f(i)`.
|
Filter.Tendsto.isBoundedUnder_ge
theorem Filter.Tendsto.isBoundedUnder_ge :
∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : BoundedGENhdsClass α]
{f : Filter ι} {u : ι → α} {a : α},
Filter.Tendsto u f (nhds a) → Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u
This theorem states that for any types `ι` and `α`, given a preorder on `α`, a topology on `α`, and a class of bounded generalized neighborhoods on `α`, if `f` is a filter on `ι` and `u` is a function from `ι` to `α` that tends to `a` under the filter `f` (i.e., `Filter.Tendsto u f (nhds a)`), then the image of the filter `f` under `u` is eventually bounded from below. In other words, there exists some `α` that is less than or equal to all elements in the image of `f` under `u` after a certain point.
More concisely: Given a preorder on `α`, a topology on `α`, and a class of bounded neighborhoods, if a filter `f` on `ι` tends to a point `a` in `α` under a function `u` from `ι` to `α`, then there exists a bound `b` in `α` such that for all `i` in `ι`, `u(i)` is bounded below by `b` when `i` belongs to the filter `f`.
|
Antitone.map_limsSup_of_continuousAt
theorem Antitone.map_limsSup_of_continuousAt :
∀ {R : Type u_4} {S : Type u_5} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
[inst_2 : OrderTopology R] [inst_3 : ConditionallyCompleteLinearOrder S] [inst_4 : TopologicalSpace S]
[inst_5 : OrderTopology S] {F : Filter R} [inst_6 : F.NeBot] {f : R → S},
Antitone f →
ContinuousAt f F.limsSup →
autoParam (Filter.IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝ →
autoParam (Filter.IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝¹ → f F.limsSup = Filter.liminf f F
The theorem `Antitone.map_limsSup_of_continuousAt` states that for any antitone function `f` mapping from a conditionally complete linear ordered space `R` to another such space `S`, if `f` is continuous at the supremum limit (`limsSup`) of a given filter `F` in `R` (which is also bounded from above and below), then the value of `f` at the `limsSup` of `F` is equal to the infimum limit (`liminf`) of the image of `F` under `f`. In other words, `f` maps the `limsSup` of `F` to the `liminf` of the image of `F` under `f`.
More concisely: For an antitone function `f` between conditionally complete linear ordered spaces `R` and `S`, if `f` is continuous at the supremum `x` of a filter `F` in `R` (bounded above and below), then `f(x) = inf { f(y) | y ∈ F }`.
|
limsup_add_const
theorem limsup_add_const :
∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
[inst_2 : OrderTopology R] (F : Filter ι) [inst_3 : F.NeBot] [inst_4 : Add R] [inst_5 : ContinuousAdd R]
[inst_6 : CovariantClass R R (Function.swap fun x y => x + y) fun x y => x ≤ y] (f : ι → R) (c : R),
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f →
Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F f → Filter.limsup (fun i => f i + c) F = Filter.limsup f F + c
The theorem `limsup_add_const` states that for any filter `F` on a type `ι` and a function `f : ι → R` from `ι` to a type `R` (where `R` is a conditionally complete linear order with a topological structure, an addition operation, and satisfies the continuous add and covariant class conditions), the limsup (the infimum of the upper bounds) of the sum of the function's values and a constant `c` over the filter equals the sum of the limsup of the function's values over the filter and the constant `c`. This is assuming that the function is both upper and lower bounded with respect to `F`. In mathematical terms, it states that `limsup (xᵢ + c) = (limsup xᵢ) + c`.
More concisely: For any filter `F` on a conditionally complete linear order `(ι, ≤)` with topology, and any upper and lower bounded function `f : ι → R` from `ι` to a type `R` with the given properties, `limsup (∑ i in F (f i + c)) = ∑ i in F (limsup fi + c)`.
|