Mathlib.Order.LiminfLimsup._auxLemma.15
theorem Mathlib.Order.LiminfLimsup._auxLemma.15 :
∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, (x ∈ ⋃ i, s i) = ∃ i, x ∈ s i
This theorem, named `_auxLemma.15` in the `Mathlib.Order.LiminfLimsup` namespace, states that for all types `α` and `ι`, and for any element `x` from `α` and any function `s` mapping from `ι` to `Set α`, the proposition "x belongs to the union over i of the sets `s i`" is equivalent to "there exists an `i` such that `x` belongs to the set `s i`". In mathematical terms, it captures the idea that an element is in the union of a collection of sets if and only if it's in at least one of the sets in the collection.
More concisely: For any type `α`, element `x` from `α`, and function `s` mapping from an index type `ι` to sets of `α`, `x` belongs to the union of `s i` for some `i` if and only if `x` is in some `s i`.
|
Filter.CompleteLatticeHom.apply_limsup_iterate
theorem Filter.CompleteLatticeHom.apply_limsup_iterate :
∀ {α : Type u_1} [inst : CompleteLattice α] (f : CompleteLatticeHom α α) (a : α),
f (Filter.limsup (fun n => (⇑f)^[n] a) Filter.atTop) = Filter.limsup (fun n => (⇑f)^[n] a) Filter.atTop
The theorem states that for a function `f` which is a morphism of complete lattices and for any element `a` from a complete lattice `α`, the limsup (limit superior) of the iterates of `a` under the function `f` is a fixed point of `f`.
In other words, if we iterate the function `f` on the element `a` infinitely many times towards positive infinity (represented by `Filter.atTop`), and then take the greatest lower bound of the set of all upper bounds of these iterates (which is the definition of limsup), the result is a value that remains unchanged under the application of `f`. This value is hence a fixed point of the function `f`.
More concisely: Let `f` be a morphism of complete lattices, then the limsup of the iterates of any element `a` in a complete lattice under `f` is a fixed point of `f`.
|
Filter.blimsup_sup_not
theorem Filter.blimsup_sup_not :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {p : β → Prop} {u : β → α},
(Filter.blimsup u f p ⊔ Filter.blimsup u f fun x => ¬p x) = Filter.limsup u f
The theorem `Filter.blimsup_sup_not` states that for any complete distributive lattice `α`, filter `f` on type `β`, predicate `p` on `β` and function `u` from `β` to `α`, the supremum (join operation) of the `blimsup` of `u` with respect to `f` and `p` and the `blimsup` of `u` with respect to `f` and the negation of `p`, is equal to the `limsup` of `u` along the filter `f`. In other words, the `limsup` of function `u` along a filter `f` is the supremum of the `blimsup` for the function `u` where predicate `p` holds, and the `blimsup` for the function `u` where the negation of predicate `p` holds.
More concisely: For any complete distributive lattice α, filter f on β, predicate p on β, and function u from β to α, the limit supremum of u along f is equal to the join of the blimsup of u with respect to f and p, and the blimsup of u with respect to f and the negation of p.
|
Filter.limsSup_le_limsSup
theorem Filter.limsSup_le_limsSup :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {f g : Filter α},
autoParam (Filter.IsCobounded (fun x x_1 => x ≤ x_1) f) _auto✝ →
autoParam (Filter.IsBounded (fun x x_1 => x ≤ x_1) g) _auto✝¹ →
(∀ (a : α), (∀ᶠ (n : α) in g, n ≤ a) → ∀ᶠ (n : α) in f, n ≤ a) → f.limsSup ≤ g.limsSup
The theorem `Filter.limsSup_le_limsSup` states that for any type `α` that forms a conditionally complete lattice, and for any filters `f` and `g` over this type, if filter `f` is co-bounded (meaning there exists an upper bound for the values eventually obtained from the filter) and filter `g` is bounded (meaning there is some value that eventually all elements from the filter are less than or equal to), and if for every element `a` of `α`, whenever every element eventually obtained from filter `g` is less than or equal to `a`, then every element eventually obtained from filter `f` is also less than or equal to `a`, then the limsup (the least upper bound of the set of limit points) of filter `f` is less than or equal to the limsup of filter `g`.
More concisely: If filters `f` and `g` over a conditionally complete lattice `α` have upper bounds, `f` is co-bounded and `g` is bounded, and for all `a` in `α`, every element eventually obtained from `g` being less than or equal to `a` implies every element eventually obtained from `f` is also less than or equal to `a`, then `limsup(f) ≤ limsup(g)`.
|
Filter.HasBasis.liminf_eq_ciSup_ciInf
theorem Filter.HasBasis.liminf_eq_ciSup_ciInf :
∀ {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [inst : ConditionallyCompleteLinearOrder α] {v : Filter ι}
{p : ι' → Prop} {s : ι' → Set ι} [inst_1 : Countable (Subtype p)] [inst_2 : Nonempty (Subtype p)],
v.HasBasis p s →
∀ {f : ι → α},
(∀ (j : Subtype p), (s ↑j).Nonempty) →
(∃ j, BddBelow (Set.range fun i => f ↑i)) → Filter.liminf f v = ⨆ j, ⨅ i, f ↑i
This theorem states that for any conditionally complete linear order `α`, and filters `v` over indices `ι` and `ι'`, given that `v` has a basis indexed by `ι'` with a corresponding set function `s : ι' → Set ι`, the liminf of any function `f : ι → α` along `v` can be written as the supremum of the infimum of `f` over the basis sets, provided two conditions are met:
1. Each basis set is nonempty.
2. There exists a basis element such that the range of `f` over that set is bounded below.
This theorem is an important result in order theory and analysis, providing a precise characterization of the liminf of a function in terms of supremum and infimum over basis sets. The theorem also employs a reparametrization trick to avoid taking the infimum of sets which are not bounded below.
More concisely: Given a conditionally complete linear order `α`, a filter `v` over indices `ι` with a nonempty, bounded-below basis `ι'` and corresponding set function `s : ι' → ι`, the liminf of any function `f : ι → α` along `v` equals the supremum of the infimum of `f` over the basis sets `s(j)`.
|
Filter.CompleteLatticeHom.apply_liminf_iterate
theorem Filter.CompleteLatticeHom.apply_liminf_iterate :
∀ {α : Type u_1} [inst : CompleteLattice α] (f : CompleteLatticeHom α α) (a : α),
f (Filter.liminf (fun n => (⇑f)^[n] a) Filter.atTop) = Filter.liminf (fun n => (⇑f)^[n] a) Filter.atTop
The theorem states that for any complete lattice `α` and any morphism `f` from `α` to `α`, the limit inferior (or `liminf`) of the iterates of any element `a` of `α` is a fixed point of the function `f`. In other words, applying `f` to the `liminf` of the sequence of `f` applied `n` times to `a` as `n` goes to infinity gives the same value as the `liminf` itself. This fixed point property is a key characteristic of limit inferior.
More concisely: For any complete lattice `α` and morphism `f` from `α` to `α`, the limit inferior of the sequence `(f^n(a))_n` is a fixed point of `f`, i.e., `f(liminf (f^n(a))) = liminf (f^n(a))`.
|
Mathlib.Order.LiminfLimsup._auxLemma.16
theorem Mathlib.Order.LiminfLimsup._auxLemma.16 :
∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, (x ∈ ⋂ i, s i) = ∀ (i : ι), x ∈ s i
This theorem states that for any type `α`, any type `ι` (which doesn't need to be a type in the traditional sense, but can be any kind of logical collection), any element `x` of type `α`, and any function `s` from `ι` to sets of `α`, the membership of `x` in the intersection over all `i` from `ι` of the sets `s i` is equivalent to the statement that for all `i` in `ι`, `x` is a member of the set `s i`. In simpler terms, an element belongs to the intersection of a collection of sets if and only if it belongs to each set in the collection.
More concisely: For any type `α`, any collection `ι`, element `x` of type `α`, and function `s : ι → sets α`, we have `x ∈ ∩ₛ i : ι, s i ↔ ∀ i, x ∈ s i`.
|
Filter.isBounded_iff
theorem Filter.isBounded_iff :
∀ {α : Type u_1} {r : α → α → Prop} {f : Filter α}, Filter.IsBounded r f ↔ ∃ s ∈ f.sets, ∃ b, s ⊆ {x | r x b} := by
sorry
The theorem states that a filter `f` over a type `α` is eventually bounded with respect to a relation `r` if and only if there exists a set `s` in the filter `f` such that there exists a bound `b` where all elements of the set `s` satisfy the relation `r` against `b`. In other words, `f` is eventually bounded in relation to `r` if there exists a set in `f` where all its elements are bounded by the same value according to `r`.
More concisely: A filter over a type is eventually bounded with respect to a relation if and only if it contains a set of elements all bounded by the same value according to that relation.
|
Filter.IsBounded.isCobounded_flip
theorem Filter.IsBounded.isCobounded_flip :
∀ {α : Type u_1} {r : α → α → Prop} {f : Filter α} [inst : IsTrans α r] [inst : f.NeBot],
Filter.IsBounded r f → Filter.IsCobounded (flip r) f
The theorem states that for any type `α`, relation `r`, and filter `f` over `α` which is transitive and not trivial (i.e., not bottom), if the filter `f` is eventually bounded with respect to `r` (meaning that eventually, all its elements are bounded by some uniform value with respect to `r`), then it is also frequently bounded in the opposite direction of `r`. In other words, the filter is co-bounded with respect to the relation obtained by flipping `r`. The flipping is performed by the function `flip`, which inverts the order of arguments in a binary function or relation, thereby inverting the direction of an order relation.
More concisely: If `f` is a transitive and non-trivial filter over type `α` that is eventually bounded with respect to relation `r`, then `f` is also co-bounded with respect to the relation `r.reverse`.
|
Filter.IsBounded.mono
theorem Filter.IsBounded.mono :
∀ {α : Type u_1} {r : α → α → Prop} {f g : Filter α}, f ≤ g → Filter.IsBounded r g → Filter.IsBounded r f := by
sorry
The theorem `Filter.IsBounded.mono` states that for any type `α`, relation `r` on `α`, and filters `f` and `g` on `α`, if `f` is a subfilter of `g` (denoted as `f ≤ g`), and `g` is eventually bounded with respect to the relation `r` (denoted as `Filter.IsBounded r g`), then `f` is also eventually bounded with respect to the same relation `r` (denoted as `Filter.IsBounded r f`). In other words, if a filter is a subset of another filter that is eventually bounded, then the subset filter is also eventually bounded.
More concisely: If `f ≤ g` are filters on a type `α` and `Filter.IsBounded r g` holds, then `Filter.IsBounded r f` also holds. (Here, `r` is a relation on `α`.)
|
Filter.isBoundedUnder_of
theorem Filter.isBoundedUnder_of :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : Filter β} {u : β → α},
(∃ b, ∀ (x : β), r (u x) b) → Filter.IsBoundedUnder r f u
The theorem `Filter.isBoundedUnder_of` states that for any types `α` and `β`, a relation `r` on `α`, a filter `f` on `β`, and a function `u` from `β` to `α`, if there exists a value `b` in `α` such that `r (u x) b` holds true for every `x` in `β`, then the image of the filter `f` under `u` is eventually bounded with respect to the relation `r`. In other words, if the function `u` is bounded by some uniform bound, then the values it takes on the elements of the filter `f` are also eventually bounded.
More concisely: If a relation is satisfied by the image of every element in a filter under a function, then the filter's image under that function is bounded with respect to the relation.
|
Monotone.isBoundedUnder_le_comp_iff
theorem Monotone.isBoundedUnder_le_comp_iff :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Nonempty β] [inst : LinearOrder β] [inst_1 : Preorder γ]
[inst_2 : NoMaxOrder γ] {g : β → γ} {f : α → β} {l : Filter α},
Monotone g →
Filter.Tendsto g Filter.atTop Filter.atTop →
(Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l f)
The theorem `Monotone.isBoundedUnder_le_comp_iff` states that for any types `α`, `β`, and `γ`, where `β` is a nonempty linear ordered set and `γ` is a preordered set with no maximum element, given a monotone function `g : β → γ` and a function `f : α → β`, and a filter `l` on `α` that represents a condition or trend, if `g` tends to infinity with the limit going to infinity, then the function `g` composed with `f` is eventually bounded under the relation `≤` with respect to `l` if and only if the function `f` is eventually bounded under the same relation with respect to `l`. In other words, the boundedness of the composition of `g` and `f` is equivalent to the boundedness of `f`, given the specified conditions on `g`.
More concisely: Given a monotone function `g : β → γ` tending to infinity, a preordered set `γ` with no max, a filter `l` on `α`, and functions `g : β → γ` and `f : α → β`, the composition `g ∘ f` is eventually bounded under `≤` with respect to `l` if and only if `f` is.
|
Filter.IsBoundedUnder.bddAbove_range
theorem Filter.IsBoundedUnder.bddAbove_range :
∀ {β : Type u_2} [inst : Preorder β] [inst_1 : IsDirected β fun x x_1 => x ≤ x_1] {f : ℕ → β},
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) Filter.atTop f → BddAbove (Set.range f)
This theorem states that for a type `β` that is preordered and is directed (i.e., for any two elements `x` and `x_1` there exists a third element that is greater than or equal to both `x` and `x_1`), if a function `f : ℕ → β` is such that the image of the filter `atTop` (which represents the limit tending to infinity) under `f` is eventually bounded under the relation `≤` (i.e., there exists a uniform bound that all elements in the image of `f` do not exceed after some point), then the range of `f` is bounded above, meaning there exists an upper bound for the set of all values that `f` can take.
More concisely: If `β` is a preordered and directed type, and `f : ℕ → β` is a function such that the image of the filter at infinity under `f` is eventually bounded, then `f` has an upper bound.
|
Filter.HasBasis.limsup_eq_ciInf_ciSup
theorem Filter.HasBasis.limsup_eq_ciInf_ciSup :
∀ {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [inst : ConditionallyCompleteLinearOrder α] {v : Filter ι}
{p : ι' → Prop} {s : ι' → Set ι} [inst_1 : Countable (Subtype p)] [inst_2 : Nonempty (Subtype p)],
v.HasBasis p s →
∀ {f : ι → α},
(∀ (j : Subtype p), (s ↑j).Nonempty) →
(∃ j, BddAbove (Set.range fun i => f ↑i)) → Filter.limsup f v = ⨅ j, ⨆ i, f ↑i
The theorem `Filter.HasBasis.limsup_eq_ciInf_ciSup` states that for any conditionally complete linear order `α`, and any filters `v` over indices `ι` and `s` over indices `ι'`, where `ι'` indices satisfying a property `p` are countable and non-empty, if `v` has a basis `p` `s`, then for any function `f` from `ι` to `α`, where for each `j` as subtype of `p`, the set `s ↑j` is non-empty, and there exists `j` such that the set of all `f ↑i` is bounded above, the limit superior (or `limsup`) of `f` along `v` is equal to the greatest lower bound (or infimum) over all `j` of the least upper bound (or supremum) over all `i` of `f ↑i`. This means that the `limsup` of `f` can be written as the infimum of supremums, even in a possibly non-complete conditionally complete linear order. Here, a reparametrization trick is used to avoid taking the supremum of sets which are not bounded above.
More concisely: In a conditionally complete linear order, if a filter has a countable basis over indices satisfying a given property, and for each index in the basis, the image of the function under consideration is bounded above and non-empty, then the limit superior of the function is equal to the infimum of the least upper bounds of the function over each index in the basis.
|
Filter.limsup_eq_iInf_iSup_of_nat'
theorem Filter.limsup_eq_iInf_iSup_of_nat' :
∀ {α : Type u_1} [inst : CompleteLattice α] {u : ℕ → α}, Filter.limsup u Filter.atTop = ⨅ n, ⨆ i, u (i + n) := by
sorry
The theorem `Filter.limsup_eq_iInf_iSup_of_nat'` states that for any function `u` from the natural numbers to a set `α` which forms a complete lattice, the limit superior (limsup) of `u` as we approach infinity (`Filter.atTop`) is equal to the infimum (greatest lower bound) over all natural numbers `n`, of the supremum (least upper bound) over all `i`, of `u(i + n)`. In simpler terms, it defines the limsup of a sequence in terms of the sequence of the 'upper parts' of the sequence shifted by `n` for all `n` in the natural numbers.
More concisely: For a complete lattice-valued function `u` from the natural numbers to a set `α`, the limsup as `n` approaches infinity is equal to the infimum over all natural numbers `n` of the supremum over all `i`, of `u(i + n)`.
|
Filter.limsup_const_bot
theorem Filter.limsup_const_bot :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β}, Filter.limsup (fun x => ⊥) f = ⊥ := by
sorry
The theorem `Filter.limsup_const_bot` states that for any given type `α` that forms a complete lattice, and for any filter `f` of type `β`, the limit superior (limsup) of a function that always returns the bottom element (`⊥`) with respect to the filter `f` is equal to the bottom element (`⊥`). This is a specific case of the `limsup_const` theorem where we don't need the assumption that `f` is not a minimal filter (`NeBot f`).
More concisely: For any complete lattice `α` and filter `f` on `α`, the limsup of a constant function mapping to the bottom element is equal to the bottom element.
|
Filter.limsSup_le_of_le
theorem Filter.limsSup_le_of_le :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {f : Filter α} {a : α},
autoParam (Filter.IsCobounded (fun x x_1 => x ≤ x_1) f) _auto✝ → (∀ᶠ (n : α) in f, n ≤ a) → f.limsSup ≤ a
The theorem `Filter.limsSup_le_of_le` states that for any type `α` that forms a conditionally complete lattice, given any filter `f` on `α` and any element `a` of `α`, if `f` is co-bounded with respect to the order relation `≤` (which is guaranteed by the `autoParam` condition) and every element `n` in the filter `f` is less than or equal to `a` (expressed as `∀ᶠ (n : α) in f, n ≤ a`), then the supremum limit (`limsSup`) of the filter `f` is less than or equal to `a`.
More concisely: If `α` is a conditionally complete lattice, `f` is a co-bounded filter on `α`, and every `n` in `f` is less than or equal to `a`, then `limsSup(f) ≤ a`.
|
Filter.limsup_le_of_le
theorem Filter.limsup_le_of_le :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {a : α},
autoParam (Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝ →
(∀ᶠ (n : β) in f, u n ≤ a) → Filter.limsup u f ≤ a
The theorem `Filter.limsup_le_of_le` states that for any types `α` and `β`, where `α` has an associated instance of `ConditionallyCompleteLattice`, and any filter `f` of type `β`, function `u` from `β` to `α`, and an element `a` of type `α`, if the image of the filter `f` under the function `u` is cobounded under the less than or equal to relation (meaning it does not tend to infinity), and it is almost everywhere (for all `n` in the filter `f`) the case that `u n` is less than or equal to `a`, then the limit superior (the infimum of the upper bounds) of the function `u` along the filter `f` is less than or equal to `a`.
More concisely: If `α` is a conditionally complete lattice, `f` is a filter on `β`, `u` is a function from `β` to `α`, and for all `n` in `f`, `u n` is less than or equal to `a` and the image of `f` under `u` is bounded above, then `⨆(u ∘ f) ≤ a`.
|
Filter.limsSup_le_limsSup_of_le
theorem Filter.limsSup_le_limsSup_of_le :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {f g : Filter α},
f ≤ g →
autoParam (Filter.IsCobounded (fun x x_1 => x ≤ x_1) f) _auto✝ →
autoParam (Filter.IsBounded (fun x x_1 => x ≤ x_1) g) _auto✝¹ → f.limsSup ≤ g.limsSup
The theorem `Filter.limsSup_le_limsSup_of_le` states that for any two filters `f` and `g` over a conditionally complete lattice `α`, if `f` is less than or equal to `g`, and assuming that `f` is eventually bounded above and `g` is eventually bounded below, then the `limsSup` (infimum of upper bounds) of `f` is less than or equal to the `limsSup` of `g`. This is a formal way to say that if one filter is "smaller" than another, then the smallest value that is greater than or equal to all elements of the first filter is less than or equal to the smallest value that is greater than or equal to all elements of the second filter.
More concisely: If `f` is a filter on a conditionally complete lattice `α` that is less than or equal to filter `g`, and both `f` and `g` are eventually bounded, then `limsSup(f) ≤ limsSup(g)`.
|
Filter.HasBasis.limsSup_eq_iInf_sSup
theorem Filter.HasBasis.limsSup_eq_iInf_sSup :
∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Sort u_6} {p : ι → Prop} {s : ι → Set α} {f : Filter α},
f.HasBasis p s → f.limsSup = ⨅ i, ⨅ (_ : p i), sSup (s i)
The theorem `Filter.HasBasis.limsSup_eq_iInf_sSup` states that for any type `α` that forms a Complete Lattice, any index type `ι`, any predicate `p` on `ι`, any function `s` mapping `ι` to sets of `α`, and any filter `f` on `α`, if the filter `f` has a basis characterized by the predicate `p` and the sets `s i`, then the limit superior (limsup) of the filter `f` equals the infimum over all `i` such that `p i` holds, of the supremum of `s i`. In mathematical notation, this is $\limsup f = \inf_{i : p(i)} \sup s_i$.
More concisely: The limit superior of a complete lattice's filter is equal to the infimum over indices with property `p` of the supremum of the associated sets. In mathematical notation: $\limsup f = \inf\_{i : p(i)} \sup s\_i$.
|
Filter.HasBasis.limsup_eq_ite
theorem Filter.HasBasis.limsup_eq_ite :
∀ {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [inst : ConditionallyCompleteLinearOrder α] {v : Filter ι}
{p : ι' → Prop} {s : ι' → Set ι} [inst_1 : Countable (Subtype p)] [inst_2 : Nonempty (Subtype p)],
v.HasBasis p s →
∀ (f : ι → α),
Filter.limsup f v =
if ∃ j, s ↑j = ∅ then sInf Set.univ
else if ∀ (j : Subtype p), ¬BddAbove (Set.range fun i => f ↑i) then sInf ∅ else ⨅ j, ⨆ i, f ↑i
This theorem, titled `Filter.HasBasis.limsup_eq_ite`, expresses the `limsup` of a function as an infimum of supremum in a conditionally complete linear order, possibly non-complete. This requires the use of a reparameterization trick to avoid taking the supremum of sets which are not bounded below.
The theorem states that for any function `f`, given a filter `v` that has a certain basis characterized by `p` and `s`, the `limsup` of the function with respect to the filter equals to the infimum of the universe set if there exists an index `j` such that the set `s` evaluated at `j` is empty. Otherwise, if for every index `j` in the subtype `p`, the set of function values is not bounded above, then the `limsup` is the infimum of an empty set. In all other cases, the `limsup` is the infimum over `j` of the supremum over `i` of the function values.
More concisely: For a function `f` and a filter `v` with basis `p` and `s`, if `s` is empty for some index `j` or the supremum of `f(i)` for all `i` in `p` is not bounded above for all `j`, then `limsup f(i) = ⨅ j, sup i in j (f i) = ⊥`, otherwise `limsup f(i) = ⨅ j, ⨆ i in p (sup i (f i))`.
|
Filter.limsup_eq
theorem Filter.limsup_eq :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} {u : β → α},
Filter.limsup u f = sInf {a | ∀ᶠ (n : β) in f, u n ≤ a}
The theorem `Filter.limsup_eq` states that for any conditionally complete lattice `α`, any type `β`, any filter `f` of type `β`, and any function `u` from `β` to `α`, the limit superior (`limsup`) of the function `u` along the filter `f` is equal to the infimum (`sInf`) of the set of all `a` in `α` for which there exists an event in the filter `f` such that for all `n` of type `β` in that event, `u n` is less than or equal to `a`. In other words, the `limsup` of `u` along `f` is the greatest lower bound of the set of `a` for which `u n ≤ a` eventually holds in `f`.
More concisely: The limit superior of a function along a filter is the greatest lower bound of values that are eventually smaller than the function for some event in the filter.
|
Filter.HasBasis.liminf_eq_ite
theorem Filter.HasBasis.liminf_eq_ite :
∀ {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [inst : ConditionallyCompleteLinearOrder α] {v : Filter ι}
{p : ι' → Prop} {s : ι' → Set ι} [inst_1 : Countable (Subtype p)] [inst_2 : Nonempty (Subtype p)],
v.HasBasis p s →
∀ (f : ι → α),
Filter.liminf f v =
if ∃ j, s ↑j = ∅ then sSup Set.univ
else if ∀ (j : Subtype p), ¬BddBelow (Set.range fun i => f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i
This theorem describes the computation of the limit inferior (or `liminf`) of a function `f` along a filter `v` in a (potentially non-complete) conditionally complete linear order. It states that if `v` has a basis `p` and `s`, then the `liminf` of `f` with respect to `v` can be written in three potential ways, depending on certain conditions.
If there exists a `j` such that the set `s` at `j` is empty, then the `liminf` is the supremum of the universal set. If for all `j` in the subtype `p`, the range of the function `f` when mapped over `i` is not bounded below, then the `liminf` is the supremum of an empty set. Otherwise, the `liminf` is the supremum of the set of all infimums of `f` at `i` over all `j`.
This theorem essentially encapsulates a reparametrization trick to avoid the issue of taking the infimum of sets which are not bounded below.
More concisely: Given a function `f` in a (potentially non-complete) conditionally complete linear order with filter `v` having basis `p` and `s`, the limit inferior of `f` with respect to `v` is the supremum of the infima of `f` at `i` over all `j` if the range of `f` at `i` is bounded below for some `j` in `p`, or the supremum of the universal set if `s` is empty, otherwise the supremum of the universal set.
|
Filter.bliminf_or_le_inf
theorem Filter.bliminf_or_le_inf :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
(Filter.bliminf u f fun x => p x ∨ q x) ≤ Filter.bliminf u f p ⊓ Filter.bliminf u f q
The theorem `Filter.bliminf_or_le_inf` states that for any types `α` and `β` where `α` is a complete lattice, for any filter `f` of type `β`, for any predicates `p` and `q` on `β`, and for any function `u` from `β` to `α`, the bounded limit inferior of the function `u` along the filter `f`, bounded by the predicate `p OR q`, is less than or equal to the infimum of the bounded limit inferior of `u` along `f` bounded by `p` and the bounded limit inferior of `u` along `f` bounded by `q`. In other words, if we take the supremum over all `a` where eventually for `f`, `a` is less than or equal to `u(x)` whenever `p(x) OR q(x)` holds, this is always less than or equal to the infimum of the similar supremums for `p(x)` and `q(x)` individually.
More concisely: For any complete lattice α, filter f on β, predicates p and q on β, and function u from β to α, the bounded limit inferior of u along f, bounded by p OR q, is less than or equal to the infimum of the bounded limit inferior of u along f, bounded by p, and the bounded limit inferior of u along f, bounded by q.
|
Filter.blimsup_sup_le_or
theorem Filter.blimsup_sup_le_or :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
Filter.blimsup u f p ⊔ Filter.blimsup u f q ≤ Filter.blimsup u f fun x => p x ∨ q x
The theorem `Filter.blimsup_sup_le_or` states that for any type `α` with a complete lattice structure, a function `u` from a type `β` to `α`, a filter `f` of `β`, and predicates `p` and `q` on `β`, the supremum of the bounded limit superior of function `u` along filter `f` bounded by predicate `p` and the bounded limit superior of function `u` along filter `f` bounded by predicate `q` is less than or equal to the bounded limit superior of function `u` along filter `f` bounded by a predicate that holds if either `p` or `q` holds. In mathematical terms, it can be written as `blimsup u f p ⊔ blimsup u f q ≤ blimsup u f (p ∨ q)`.
More concisely: For any complete lattice `α` and filter `f` on a type `β`, the bounded limit superior of a function `u` from `β` to `α` along `f` bounded by predicates `p` and `q` satisfies `blimsup u f p ⊔ blimsup u f q ≤ blimsup u f (p ∨ q)`.
|
Filter.IsBoundedUnder.comp
theorem Filter.IsBoundedUnder.comp :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {l : Filter γ} {q : β → β → Prop} {u : γ → α}
{v : α → β},
(∀ (a₀ a₁ : α), r a₀ a₁ → q (v a₀) (v a₁)) → Filter.IsBoundedUnder r l u → Filter.IsBoundedUnder q l (v ∘ u)
This theorem states that given types α, β, and γ, a relation 'r' on α, a filter 'l' over γ, a relation 'q' on β, a function 'u' from γ to α, and a function 'v' from α to β, if for any two elements a₀, a₁ of type α, the relation 'r' on a₀ and a₁ implies the relation 'q' on the images of a₀ and a₁ under 'v', and if the image of the filter 'l' under 'u' is eventually bounded with respect to 'r', then the image of the filter 'l' under the composition of 'v' and 'u' is eventually bounded with respect to 'q'. In other words, the boundedness condition under a function and a relation can be maintained under function composition and relation implication.
More concisely: If a filter is eventually bounded under a relation-preserving function composed with a function whose image is eventually bounded under a relation, then the image of the filter under the composition is eventually bounded under the relation.
|
Filter.blimsup_and_le_inf
theorem Filter.blimsup_and_le_inf :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
(Filter.blimsup u f fun x => p x ∧ q x) ≤ Filter.blimsup u f p ⊓ Filter.blimsup u f q
The theorem `Filter.blimsup_and_le_inf` states that for any complete lattice `α`, filter `f` on type `β`, predicates `p` and `q` on `β`, and a function `u` mapping `β` to `α`, the bounded limit superior (blimsup) of `u` along `f`, bounded by the conjunction of predicates `p` and `q`, is less than or equal to the infimum of the blimsup of `u` along `f` bounded by `p` and the blimsup of `u` along `f` bounded by `q`. In other words, this theorem shows that the blimsup along a filter, when bounded by the conjunction of two predicates, is controlled by the individual blimsups for each of the predicates.
More concisely: For any complete lattice `α`, filter `f` on type `β`, predicates `p` and `q` on `β`, and a function `u` mapping `β` to `α`, the blimsup of `u` along `f`, bounded by the conjunction of `p` and `q`, is less than or equal to the infimum of the blimsups of `u` along `f` bounded by `p` and the blimsup of `u` along `f` bounded by `q`.
|
Filter.cofinite.blimsup_set_eq
theorem Filter.cofinite.blimsup_set_eq :
∀ {α : Type u_1} {ι : Type u_4} {p : ι → Prop} {s : ι → Set α},
Filter.blimsup s Filter.cofinite p = {x | {n | p n ∧ x ∈ s n}.Infinite}
The theorem `Filter.cofinite.blimsup_set_eq` states that for any types `α` and `ι`, any predicate `p` over `ι`, and any function `s` from `ι` to a set of `α`, the bounded limit superior (blimsup) of the function `s` along the cofinite filter and bounded by the predicate `p` is equal to the set of `x` such that the set of `n` for which `p n` holds and `x` is in `s n` is infinite. In other words, the theorem describes a connection between the concept of blimsup along the cofinite filter and the condition of an infinite set within the context of a predicate and a function to sets.
More concisely: The theorem `Filter.cofinite.blimsup_set_eq` asserts that the bounded limit superior of a function from an index set to a type along the cofinite filter is equal to the set of elements in the image of the function for which the index set restricted to the satisfying indices forms an infinite set with respect to the given predicate.
|
Filter.liminf_le_liminf
theorem Filter.liminf_le_liminf :
∀ {β : Type u_2} {α : Type u_6} [inst : ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β},
(∀ᶠ (a : α) in f, u a ≤ v a) →
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝ →
autoParam (Filter.IsCoboundedUnder (fun x x_1 => x ≥ x_1) f v) _auto✝¹ →
Filter.liminf u f ≤ Filter.liminf v f
The theorem `Filter.liminf_le_liminf` states that for any types `β` and `α`, and under the condition that `β` is a conditionally complete lattice, given filter `f` on `α` and two functions `u` and `v` from `α` to `β`, if `u a` is less than or equal to `v a` for all `a` in the filter `f`, the lower limit (liminf) of `u` along the filter `f` is less than or equal to the lower limit of `v` along the same filter. This also assumes that the image of the filter `f` under `u` is eventually bounded above (expressed using `autoParam` and `Filter.IsBoundedUnder`), and the image of `f` under `v` is not tending to negative infinity (expressed using `autoParam` and `Filter.IsCoboundedUnder`).
More concisely: If `β` is a conditionally complete lattice, filter `f` on `α` has an eventual upper bound for the image under `u`, and the image under `v` is not tending to negative infinity, then `liminf(u) ≤ liminf(v)` for functions `u` and `v` from `α` to `β` satisfying `u a ≤ v a` for all `a` in `f`.
|
OrderIso.limsup_apply
theorem OrderIso.limsup_apply :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_6} [inst : ConditionallyCompleteLattice β]
[inst_1 : ConditionallyCompleteLattice γ] {f : Filter α} {u : α → β} (g : β ≃o γ),
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝ →
autoParam (Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝¹ →
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝² →
autoParam (Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝³ →
g (Filter.limsup u f) = Filter.limsup (fun x => g (u x)) f
The theorem `OrderIso.limsup_apply` states that for any types `α`, `β`, and `γ` with `β` and `γ` being conditionally complete lattices and given a filter `f` on type `α` and a function `u` from `α` to `β`, if an order isomorphism `g` from `β` to `γ` exists, then under certain conditions, the limsup (infimum of the upper bounds) of the function `u` along the filter `f` after being mapped by `g` is equal to the image of the limsup of `u` along `f` under `g`.
The conditions that need to be satisfied are that the image of the filter `f` under `u` and under the composition of `g` and `u` are both bounded and cobounded under the less than or equal to relation. In other words, there exists some uniform bound that all elements eventually do not exceed (bounded), and there is a lower limit that the elements do not infinitely descend below (cobounded).
More concisely: Given filter `f` on type `α`, function `u` from `α` to conditionally complete lattices `β` and `γ`, and order isomorphism `g` from `β` to `γ`, if the images of `f` under `u` and `g ∘ u` are both bounded and cobounded, then `limsup(g(limsup(u(x)|x ∈ f))) = limsup(u(x)|x ∈ f)`.
|
Filter.limsup_le_limsup
theorem Filter.limsup_le_limsup :
∀ {β : Type u_2} {α : Type u_6} [inst : ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β},
f.EventuallyLE u v →
autoParam (Filter.IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝ →
autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝¹ →
Filter.limsup u f ≤ Filter.limsup v f
The theorem `Filter.limsup_le_limsup` states that for any given types `β` and `α`, where `β` is a conditionally complete lattice, and any filter `f` on `α` with functions `u` and `v` from `α` to `β`, if `u` is less than or equal to `v` for all elements in the filter `f`, and if the image of `f` under `u` is not tending towards infinity (i.e., it is cobounded), and the image of `f` under `v` is eventually bounded, then the upper limit (limsup) of `u` along `f` is less than or equal to the upper limit (limsup) of `v` along `f`. In mathematical terms, if $u \leq v$ almost everywhere on $f$, and $u$ is cobounded and $v$ is bounded under $f$, then $\limsup_{x \in f} u(x) \leq \limsup_{x \in f} v(x)$.
More concisely: If $u \leq v$ almost everywhere in a cobounded filter $f$ over a conditionally complete lattice $\beta$, then $\limsup_{x \in f} u(x) \leq \limsup_{x \in f} v(x)$.
|
Filter.not_isBoundedUnder_of_tendsto_atTop
theorem Filter.not_isBoundedUnder_of_tendsto_atTop :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : NoMaxOrder β] {f : α → β} {l : Filter α}
[inst_2 : l.NeBot], Filter.Tendsto f l Filter.atTop → ¬Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
The theorem `Filter.not_isBoundedUnder_of_tendsto_atTop` states that for any types α and β, whereby β is a preorder and also has no maximum element, and given a function `f` from α to β and a filter `l` on α that is not "bottom", if the function `f` tends to infinity (represented by `Filter.atTop`) for the filter `l`, then the image of the filter `l` under `f` is not eventually bounded with respect to the relation "less than or equal to". In simpler words, if the image of `f` under the filter `l` tends to infinity, then there doesn't exist a uniform bound for the values of `f` as `l` tends towards infinity.
More concisely: If `f` is a function from type `α` to preorder `β` without a maximum element, `l` is a non-bottom filter on `α`, and `f` tends to infinity under `l`, then `Image l f` is unbounded in `β`.
|
Filter.IsBoundedUnder.bddAbove_range_of_cofinite
theorem Filter.IsBoundedUnder.bddAbove_range_of_cofinite :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : IsDirected β fun x x_1 => x ≤ x_1] {f : α → β},
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) Filter.cofinite f → BddAbove (Set.range f)
This theorem states that for any types `α` and `β`, where `β` has an order and is directed, and any function `f` mapping from `α` to `β`, if the function `f` is bounded under the cofinite filter with respect to the preorder relation (i.e., every element from the cofinite filter applied to `f` is less than or equal to some fixed value eventually), then the set of all values that `f` can take (the range of `f`) is bounded above. In other words, there exists an upper bound for all possible outputs of `f`.
More concisely: If `α` is any type, `β` is a type with an order and directed, and `f` is a function from `α` to `β` that is bounded under the cofinite filter of `β`, then the range of `f` has an upper bound.
|
Filter.blimsup_eq_iInf_biSup
theorem Filter.blimsup_eq_iInf_biSup :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α},
Filter.blimsup u f p = ⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), u b
The theorem `Filter.blimsup_eq_iInf_biSup` states that for any complete lattice `α`, any filter `f` on `β`, any predicate `p` on `β`, and any function `u` from `β` to `α`, the bounded limit superior (`blimsup`) of the function `u` along the filter `f` and bounded by the predicate `p` is equal to the infimum over all sets `s` in the filter `f`, of the supremum over all elements `b` such that `p b` and `b` is in `s`, of `u b`. In other words, the bounded limit superior of `u` is the least upper bound of the set of all `u b` where `b` satisfies `p` and `b` is in some set `s` from the filter `f`.
More concisely: The bounded limit superior of a function along a filter, with respect to a predicate, equals the infimum of sets in the filter, where each set's supremum is the function's value at an element satisfying the predicate.
|
Filter.IsCobounded.mk
theorem Filter.IsCobounded.mk :
∀ {α : Type u_1} {r : α → α → Prop} {f : Filter α} [inst : IsTrans α r] (a : α),
(∀ s ∈ f, ∃ x ∈ s, r a x) → Filter.IsCobounded r f
The theorem `Filter.IsCobounded.mk` states that for any type `α`, a relation `r` on `α`, a filter `f` on `α`, and a transitivity instance for the relation `r`, if you have an element `a` of `α` such that for every set `s` in the filter `f` there exists an element `x` in set `s` for which the relation `r` holds between `a` and `x`, then the filter `f` is cobounded with respect to the relation `r`. This theorem only proves one direction of the implication because the other direction is not true for the trivial filter.
More concisely: If for every set in a filter on a type and for every element in the set, there exists an element related to the given element by the filter, then the filter is cobounded with respect to the relation. (Assumes the relation is transitive.)
|
Filter.limsup_le_iSup
theorem Filter.limsup_le_iSup :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {u : β → α},
Filter.limsup u f ≤ ⨆ n, u n
The theorem `Filter.limsup_le_iSup` states that for any function `u` from a type `β` to a type `α` (where `α` is a complete lattice), and for any filter `f` on `β`, the limit superior (`limsup`) of `u` along `f` is less than or equal to the supremum (denoted by `⨆ n, u n`) of the values of `u`. In simpler terms, the highest value that `u` can approach using the filter `f` is always less than or equal to the highest value `u` can take.
More concisely: For any complete lattice α, function u from a filter f on β to α, the limsup of u along f (limsup u f) is less than or equal to the supremum of u (⨆ n, u n).
|
Mathlib.Order.LiminfLimsup._auxLemma.19
theorem Mathlib.Order.LiminfLimsup._auxLemma.19 : ∀ {b a : Prop}, (∃ (_ : a), b) = (a ∧ b)
This theorem, named `Mathlib.Order.LiminfLimsup._auxLemma.19`, states that for any two propositions `a` and `b`, the existence of `b` given `a` is equivalent to the conjunction of `a` and `b`. In other words, saying "there exists an `a` such that `b` is true" is the same as saying "`a` is true and `b` is true".
More concisely: The theorem `Mathlib.Order.LiminfLimsup._auxLemma.19` in Lean 4 asserts that for all propositions `a` and `b`, `(∃x, a x) ∧ b` is equivalent to `a ∧ b`.
|
Filter.cofinite.liminf_set_eq
theorem Filter.cofinite.liminf_set_eq :
∀ {α : Type u_1} {ι : Type u_4} {s : ι → Set α}, Filter.liminf s Filter.cofinite = {x | {n | x ∉ s n}.Finite} := by
sorry
This theorem states that for any type `α` and index type `ι`, and any family `s` of sets of type `α` indexed by `ι`, the limit inferior (liminf) of the function `s` along the cofinite filter equals the set of elements `x` that lie outside the sets `s n` only finitely often. In other words, `x` is in the liminf if and only if there are only finitely many indices `n` such that `x` is not in the set `s n`.
More concisely: The theorem asserts that the limit inferior of a family of sets `s` indexed by `ι` equals the set of elements not excluded from infinitely many sets `s n`.
|
Filter.limsup_congr
theorem Filter.limsup_congr :
∀ {β : Type u_2} {α : Type u_6} [inst : ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β},
(∀ᶠ (a : α) in f, u a = v a) → Filter.limsup u f = Filter.limsup v f
The theorem `Filter.limsup_congr` states that for any types `β` and `α` with `β` being a conditionally complete lattice, and for any filter `f` on `α` and any two functions `u` and `v` from `α` to `β`, if it is the case that for all `a` eventually in `f`, `u(a)` equals `v(a)`, then the limit superior (limsup) of `u` along `f` is equal to the limit superior of `v` along `f`.
In less technical terms, it says that if two functions are eventually the same for all elements in a certain filter, then the limsup of the two functions over that filter are also the same.
More concisely: If `β` is a conditionally complete lattice and `f` is a filter on `α`, then for functions `u` and `v` from `α` to `β` with `u(a) = v(a)` for all `a` eventually in `f`, it holds that `limsup(u) = limsup(v)` along `f`.
|
Filter.cofinite.limsup_set_eq
theorem Filter.cofinite.limsup_set_eq :
∀ {α : Type u_1} {ι : Type u_4} {s : ι → Set α}, Filter.limsup s Filter.cofinite = {x | {n | x ∈ s n}.Infinite}
The theorem `Filter.cofinite.limsup_set_eq` states that for any type `α` and `ι`, and for any function `s` from `ι` to the sets of `α`, the limsup of `s` along the cofinite filter is equal to the set of elements `x` such that, the set of `n` for which `x` belongs to `s(n)` is infinite. In simpler terms, this theorem states that the limit superior (limsup) of a family of sets `s` with respect to the cofinite filter is the set of elements that belong to infinitely many sets in the family `s`.
More concisely: The limsup of a family of sets with respect to the cofinite filter is the set of elements belonging to infinitely many sets in the family.
|
Filter.limsup_eq_iInf_iSup_of_nat
theorem Filter.limsup_eq_iInf_iSup_of_nat :
∀ {α : Type u_1} [inst : CompleteLattice α] {u : ℕ → α},
Filter.limsup u Filter.atTop = ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), u i
This theorem states that for any function `u` from the natural numbers to a complete lattice `α`, the limit superior (`limsup`) of `u` as it approaches infinity is equal to the greatest lower bound (`infimum`) over all natural numbers `n`, of the least upper bounds (`supremum`) over all `i` that are greater than or equal to `n`, of `u(i)`. In other words, as we consider `u` over larger and larger sets of natural numbers, the smallest of the largest values that `u` takes on (i.e., the `limsup`) is equal to the smallest value among all the largest values of `u` over all sets of natural numbers starting from any given `n`.
More concisely: The limit superior of a function `u` from natural numbers to a complete lattice `α` equals the infimum over all natural numbers `n` of the supremum over all `i ≥ n` of `u(i)`.
|
Filter.limsup_eq_iInf_iSup
theorem Filter.limsup_eq_iInf_iSup :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {u : β → α},
Filter.limsup u f = ⨅ s ∈ f, ⨆ a ∈ s, u a
The theorem `Filter.limsup_eq_inf_sup` states that in a complete lattice, the limit superior (limsup) of a function is equal to the greatest lower bound (infimum) over all sets `s` in the filter of the least upper bound (supremum) of the function over `s`. In other words, for any complete lattice `α`, any filter `f` of `β`, and any function `u` mapping `β` to `α`, the limsup of `u` with respect to `f` is the infimum of the set of all supremums of `u` over all `s` in `f`.
More concisely: In a complete lattice, the limit superior of a function with respect to a filter is the infimum of the supremums of the function over all sets in the filter.
|
OrderIso.isBoundedUnder_le_comp
theorem OrderIso.isBoundedUnder_le_comp :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {l : Filter γ}
{u : γ → α},
(Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => e (u x)) ↔
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l u
The theorem `OrderIso.isBoundedUnder_le_comp` states that for any three types `α`, `β`, and `γ`, with `α` and `β` equipped with preorders, given an order isomorphism `e` from `α` to `β`, a filter `l` on `γ`, and a function `u` from `γ` to `α`, the image of the filter `l` under the function `x => e (u x)` is eventually bounded with respect to the less than or equal to relation (i.e., there exists some uniform bound from a certain point onwards) if and only if the image of filter `l` under the function `u` is eventually bounded with respect to the less than or equal to relation. In other words, the boundedness of the mapped filter under the composition of `e` and `u` is equivalent to the boundedness of the mapped filter under `u` alone.
More concisely: Given an order isomorphism between preordered types `α` and `β`, and a filter on a third type `γ`, the image of the filter under the composition of the order isomorphism with a function from `γ` to `α` is eventually bounded if and only if the image of the filter under the function alone is eventually bounded.
|
Filter.blimsup_eq_limsup
theorem Filter.blimsup_eq_limsup :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop},
Filter.blimsup u f p = Filter.limsup u (f ⊓ Filter.principal {x | p x})
The theorem `Filter.blimsup_eq_limsup` asserts that for any type `α` that forms a conditionally complete lattice, any filter `f` of type `β`, any function `u` from `β` to `α`, and any predicate `p` on `β`, the bounded limit superior (`blimsup`) of the function `u` along the filter `f`, bounded by the predicate `p`, is equal to the limit superior (`limsup`) of the function `u` along the infimum of the filter `f` and the principal filter of the set of elements satisfying the predicate `p`. In other words, it states that the infimum of all upper bounds `a` that are eventually reached by `u` at points where `p` holds, is the same as the infimum of all upper bounds that are eventually reached by `u` along the set of points where `p` is true.
More concisely: For any conditionally complete lattice α, filter f on β, function u from β to α, and predicate p on β, the bounded limit superior of u along f, bounded by p, equals the limit superior of u along the infimum of f and the principal filter of elements satisfying p.
|
Filter.liminf_const_top
theorem Filter.liminf_const_top :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β}, Filter.liminf (fun x => ⊤) f = ⊤ := by
sorry
This theorem, `Filter.liminf_const_top`, states that for any given complete lattice `α`, any type `β`, and any filter `f` of type `β`, the limit inferior (or `liminf`) of the constant function that always returns the top element (`⊤`) of the lattice, when taken along the filter `f`, is equal to the top element (`⊤`) of the lattice. This holds without needing the assumption that the filter `f` is not the bottom element (`⊥` or `NeBot`).
More concisely: For any complete lattice `α` and filter `f` of type `β`, the limit inferior of the constant function mapping to the top element of `α` along filter `f` equals the top element of `α`.
|
Filter.liminf_eq_iSup_iInf
theorem Filter.liminf_eq_iSup_iInf :
∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {u : β → α},
Filter.liminf u f = ⨆ s ∈ f, ⨅ a ∈ s, u a
In the context of a complete lattice, this theorem states that the lower limit (or `liminf`) of a function `u` as it approaches a filter `f` is equal to the supremum over all sets `s` in the filter `f` of the infimum of `u` over the set `s`. This means that for every set `s` in the filter `f`, we calculate the least value of the function `u` over the set `s`, and then among all these least values, we find the greatest one. This greatest least value is exactly the `liminf` of the function `u` with respect to the filter `f`.
More concisely: In a complete lattice, the liminf of a function with respect to a filter is equal to the supremum of the infima of the function over each set in the filter.
|