Filter.tendsto_abs_atTop_atTop
theorem Filter.tendsto_abs_atTop_atTop :
∀ {α : Type u_3} [inst : LinearOrderedAddCommGroup α], Filter.Tendsto abs Filter.atTop Filter.atTop
The theorem `Filter.tendsto_abs_atTop_atTop` states that for any type `α` which is a linearly ordered additive commutative group, the absolute value function `abs` has a limit of positive infinity as its argument approaches positive infinity. In other words, as we take larger and larger values of `x` (approaching positive infinity), the absolute value of `x` (denoted as `|x|`) also approaches positive infinity. Using the $\lim_{x\to+\infty}$ notation, this can be written as $\lim_{x\to+\infty}|x|=+\infty$.
More concisely: For any linearly ordered additive commutative group type `α`, the absolute value function `abs` on `α` is unbounded above and approaches positive infinity as the argument approaches positive infinity.
|
Filter.tendsto_const_mul_atTop_iff_neg
theorem Filter.tendsto_const_mul_atTop_iff_neg :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [inst_1 : l.NeBot],
Filter.Tendsto f l Filter.atBot → (Filter.Tendsto (fun x => r * f x) l Filter.atTop ↔ r < 0)
The theorem states that for any types `α` and `β` where `α` is a linearly ordered field, and given a nontrivial filter `l` on `β`, a function `f` from `β` to `α`, and a scalar `r` in `α`, if the function `f` has a limit of negative infinity as the argument approaches the points determined by the filter `l`, then the function obtained by multiplying `f` by the scalar `r` tends to infinity if and only if the scalar `r` is less than zero.
More concisely: For a linearly ordered field `α` and a nontrivial filter `l` on type `β`, if function `f` from `β` to `α` has limit -∞ as arguments approach filter `l`, then `rf` tends to ∞ if and only if `r` is negative.
|
Filter.tendsto_mul_const_atBot_of_pos
theorem Filter.tendsto_mul_const_atBot_of_pos :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α},
0 < r → (Filter.Tendsto (fun x => f x * r) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot)
The theorem `Filter.tendsto_mul_const_atBot_of_pos` states that for any positive real number `r`, a function `f` that maps an arbitrary type `β` to a linearly ordered field `α` tends towards negative infinity (`Filter.atBot`) along a certain filter `l` if and only if the function obtained by multiplying `f` by `r` tends towards negative infinity along the same filter. Essentially, the rate of decrease towards negative infinity is not affected by multiplication with a positive constant.
More concisely: Given a filter `l` on a type `β`, a linearly ordered field `α`, and a function `f` from `β` to `α`, if `r` is a positive real number and `f` tends towards negative infinity along `l`, then `rf` also tends towards negative infinity along `l`.
|
Filter.tendsto_atBot_atBot
theorem Filter.tendsto_atBot_atBot :
∀ {α : Type u_3} {β : Type u_4} [inst : Nonempty α] [inst : SemilatticeInf α] [inst_1 : Preorder β] {f : α → β},
Filter.Tendsto f Filter.atBot Filter.atBot ↔ ∀ (b : β), ∃ i, ∀ a ≤ i, f a ≤ b
The theorem `Filter.tendsto_atBot_atBot` states that for any function `f` mapping from a type `α`, which is nonempty and forms a semilattice under an infimum operation, to a type `β` with a preorder, then `f` tends to negative infinity (represented by `Filter.atBot`) as its argument tends to negative infinity if and only if for any value `b` of type `β`, there exists a value `i` such that for all `a` less than or equal to `i`, the image `f(a)` is less than or equal to `b`. This relates the concept of a function tending towards negative infinity in both its domain and range with a universal quantification over a property involving all elements below a certain threshold in the domain.
More concisely: For a function from a semilattice to a preordered type, if the image of every element less than or equal to some index approaches the minimum element at the range side, then the function tends to the minimum element at the range as the domain element tends to negative infinity.
|
Filter.tendsto_pow_atTop
theorem Filter.tendsto_pow_atTop :
∀ {α : Type u_3} [inst : OrderedSemiring α] {n : ℕ},
n ≠ 0 → Filter.Tendsto (fun x => x ^ n) Filter.atTop Filter.atTop
The theorem `Filter.tendsto_pow_atTop` states that for any positive natural number `n`, the monomial function `x^n` tends to positive infinity as `x` tends to positive infinity. This is expressed in the context of ordered semiring. The function `x^n` is said to tend towards infinity, if for every neighborhood `a` around infinity, there exists some `x` such that for all `x'` greater than `x`, `x'^n` is in the neighborhood `a`. A corresponding statement for real powers exists as `tendsto_rpow_atTop`.
More concisely: For every positive natural number `n`, the function `x => x^n` tends to positive infinity as `x` approaches positive infinity in an ordered semiring.
|
Filter.atTop_Ioi_eq
theorem Filter.atTop_Ioi_eq :
∀ {α : Type u_3} [inst : SemilatticeSup α] (a : α), Filter.atTop = Filter.comap Subtype.val Filter.atTop
This theorem states that for any semi-lattice (a partially ordered set with a supremum operation) of type α and any element `a` of type α, the "atTop" filter on the open interval greater than `a` (`Ioi a`) is equivalent to the "atTop" filter in the entire order, preprocessed by the function `Subtype.val`. Here, "atTop" filter represents the limit heading towards positive infinity in an ordered set, and `Subtype.val` is a function that retrieves the underlying element from a subtype. Essentially, this theorem connects the limit behavior on an infinite subset of the semi-lattice to that on the whole semi-lattice.
More concisely: For any semi-lattice and its element `a`, the "atTop" filters on `Ioi a` and the entire order are equivalent after applying `Subtype.val`.
|
Filter.tendsto_atBot_of_monotone_of_filter
theorem Filter.tendsto_atBot_of_monotone_of_filter :
∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder ι] [inst_1 : Preorder α] {l : Filter ι} {u : ι → α},
Monotone u → ∀ [inst_2 : l.NeBot], Filter.Tendsto u l Filter.atBot → Filter.Tendsto u Filter.atBot Filter.atBot
This theorem states that if we have a monotone function `u` mapping from type `ι` to type `α`, both of which are preordered, and this function tends to `-∞` (represented by `atBot`) along any non-trivial filter `l`, then the function `u` will also tend to `-∞` along `atBot`. In other words, if `u` decreases without bound for some specific progression represented by the filter `l`, then it will decrease without bound in general.
More concisely: If `u` is a monotone function from preordered type `ι` to type `α`, and `u` tends to `-∞` along any non-trivial filter `l` on `ι`, then `u` tends to `-∞` at the bottom element `atBot` of `ι`.
|
Mathlib.Order.Filter.AtTopBot._auxLemma.18
theorem Mathlib.Order.Filter.AtTopBot._auxLemma.18 :
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : NoMaxOrder α] (x : α) (l : Filter β)
[inst_2 : l.NeBot], Filter.Tendsto (fun x_1 => x) l Filter.atTop = False
This theorem states that for all types `α` and `β` where `α` has a preorder structure and does not have a maximum element (`NoMaxOrder α`), and for every element `x` of type `α` and every non-bottom filter `l` of type `β` (`Filter.NeBot l`), the constant function from `β` to `α` that always returns `x` does not tend towards infinity (`Filter.atTop`) as the inputs tend towards any neighborhood under the filter `l`. In other words, there is no filter `l` under which the preimage of any neighborhood of infinity is a neighborhood of `x`.
More concisely: For any type `α` with no maximum element and filter `l` over type `β`, the constant function from `β` to `α` does not tend towards infinity under filter `l`.
|
Filter.map_add_atTop_eq_nat
theorem Filter.map_add_atTop_eq_nat : ∀ (k : ℕ), Filter.map (fun a => a + k) Filter.atTop = Filter.atTop
This theorem states that for any natural number `k`, the mapping of the filter `atTop` (representing the limit towards infinity on an ordered set) through the function `a => a + k` results in the same `atTop` filter. In other words, adding a constant `k` to each element of an infinite sequence does not change the fact that the sequence grows without bound.
More concisely: For any natural number `k`, the `atTop` filter of the function `x => x + k` over an ordered set is equal to the `atTop` filter of the identity function.
|
Mathlib.Order.Filter.AtTopBot._auxLemma.26
theorem Mathlib.Order.Filter.AtTopBot._auxLemma.26 :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [inst_1 : l.NeBot],
Filter.Tendsto (fun x => r * f x) l Filter.atTop =
(0 < r ∧ Filter.Tendsto f l Filter.atTop ∨ r < 0 ∧ Filter.Tendsto f l Filter.atBot)
The theorem `Mathlib.Order.Filter.AtTopBot._auxLemma.26` states that for any types `α` and `β`, where `α` is a linearly ordered field, a filter `l` on `β`, a function `f` from `β` to `α`, and a real number `r`, if the filter `l` is not a bottom filter, then the function `f` multiplied by `r` tends towards infinity (`Filter.atTop`) as `l` tends towards infinity if and only if either `r` is positive and `f` tends towards infinity as `l` tends towards infinity, or `r` is negative and `f` tends towards negative infinity (`Filter.atBot`) as `l` tends towards infinity.
More concisely: For a linearly ordered field `α`, a filter `l` on `β`, a function `f` from `β` to `α`, and a real number `r`, if `l` is not a bottom filter, then `f` multiplied by `r` tends towards infinity (`Filter.atTop`) if `r` is positive and `f` does, or tends towards negative infinity (`Filter.atBot`) if `r` is negative.
|
Filter.tendsto_atTop_add_const_left
theorem Filter.tendsto_atTop_add_const_left :
∀ {α : Type u_3} {β : Type u_4} [inst : OrderedAddCommGroup β] (l : Filter α) {f : α → β} (C : β),
Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => C + f x) l Filter.atTop
The theorem `Filter.tendsto_atTop_add_const_left` states that for any types `α` and `β`, where `β` is an ordered additive commutative group, any filter `l` on `α`, any function `f` from `α` to `β`, and any constant `C` of type `β`, if the function `f` tends to infinity (`Filter.atTop`) as we approach the points defined by the filter `l`, then the function which adds the constant `C` to each value of `f` also tends to infinity as we approach the points defined by `l`. In mathematical terms, if $\lim_{x \to l} f(x) = \infty$, then $\lim_{x \to l} (C + f(x)) = \infty$.
More concisely: If a filter `l` on type `α` and a function `f:` `α` → `β` (where `β` is an ordered additive commutative group) tend to infinity at `l`, then the function `C + f` also tends to infinity at `l`, for any constant `C` of type `β`.
|
Filter.Tendsto.eventually_gt_atTop
theorem Filter.Tendsto.eventually_gt_atTop :
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] [inst_1 : NoMaxOrder β] {f : α → β} {l : Filter α},
Filter.Tendsto f l Filter.atTop → ∀ (c : β), ∀ᶠ (x : α) in l, c < f x
The theorem `Filter.Tendsto.eventually_gt_atTop` states that for any types `α` and `β`, where `β` is a type with a preorder and having no maximum element, if a function `f : α → β` tends towards `Filter.atTop` (or in other words, the function `f` approaches infinity) for any filter `l` of type `α`, then for any value `c` of type `β`, eventually (for all elements `x` in the filter `l` beyond a certain point), the value of the function `f(x)` is greater than `c`. Essentially, this theorem guarantees that a function which tends to infinity will eventually surpass any given value.
More concisely: For any filter \(l\) on type \(\alpha\) and any \(c \in \beta\), without a maximum element, if \(f : \alpha \to \beta\) tends to \(\operatorname{atTop}\) for filter \(l\), then for all \(x \in l\) beyond some index, we have \(f(x) > c\).
|
Filter.eventually_gt_atTop
theorem Filter.eventually_gt_atTop :
∀ {α : Type u_3} [inst : Preorder α] [inst_1 : NoMaxOrder α] (a : α), ∀ᶠ (x : α) in Filter.atTop, a < x
The theorem `Filter.eventually_gt_atTop` states that for any given type `α`, which has a `Preorder` and `NoMaxOrder` instance, and for any element `a` of type `α`, eventually (for some point and all points beyond that), elements `x` of type `α` will satisfy the condition `a < x` when moving towards the limit `∞` (represented by the filter `Filter.atTop`). In other words, this theorem guarantees that given any element in an ordered set with no maximum element, there will always be elements greater than it as we approach infinity.
More concisely: For any element `a` in an ordered set without a maximum element, there exists a point beyond which all elements are strictly greater than `a`.
|
Filter.HasAntitoneBasis.subbasis_with_rel
theorem Filter.HasAntitoneBasis.subbasis_with_rel :
∀ {α : Type u_3} {f : Filter α} {s : ℕ → Set α},
f.HasAntitoneBasis s →
∀ {r : ℕ → ℕ → Prop},
(∀ (m : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, r m n) →
∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)
This theorem, `Filter.HasAntitoneBasis.subbasis_with_rel`, states that for any type `α` and a filter `f` of this type, if there exists an antitone basis `s` (a sequence of sets indexed by natural numbers) for this filter, and a relation `r` on natural numbers such that for every natural number `m`, there's a natural number `n` greater than `m` satisfying `r m n` (in other words, the set of such `n` is dense in the filter towards positive infinity), then there exists a strictly increasing function `φ` from natural numbers to natural numbers such that `m < n` implies `r (φ m) (φ n)`, and the composition of `s` and `φ` forms an antitone basis for the filter `f`. In essence, this theorem provides a way to extract a subbasis from an antitone basis, where the subbasis decreases "sufficiently fast".
More concisely: Given a type `α`, a filter `f` on `α`, an antitone basis `s` for `f`, and a dense relation `r` on natural numbers, there exists a strictly increasing function `φ` and a subbasis `s' = {s ∘ φ (i) | i ∈ ℕ}` such that `s'` is antitone for `f`.
|
Filter.tendsto_atTop_add_const_right
theorem Filter.tendsto_atTop_add_const_right :
∀ {α : Type u_3} {β : Type u_4} [inst : OrderedAddCommGroup β] (l : Filter α) {f : α → β} (C : β),
Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x + C) l Filter.atTop
This theorem asserts that for any type `α`, type `β` that forms an ordered commutative additive group, a filter `l` on `α`, a function `f` from `α` to `β` and an element `C` of `β`, if `f` tends to infinity (as represented by `Filter.atTop`) along the filter `l`, then the function that adds `C` to `f(x)` (i.e., `f(x) + C`) also tends to infinity along the same filter `l`. In mathematical terms, if $\lim_{x \to l} f(x) = \infty$, then $\lim_{x \to l} (f(x) + C) = \infty$.
More concisely: If a function from an ordered commutative additive group to itself tends to infinity along a filter, then the function translated by a constant also tends to infinity along the same filter.
|
Filter.tendsto_atTop_add_nonneg_left'
theorem Filter.tendsto_atTop_add_nonneg_left' :
∀ {α : Type u_3} {β : Type u_4} [inst : OrderedAddCommMonoid β] {l : Filter α} {f g : α → β},
(∀ᶠ (x : α) in l, 0 ≤ f x) →
Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x + g x) l Filter.atTop
The theorem `Filter.tendsto_atTop_add_nonneg_left'` states that, given a preordered additive commutative monoid `β` and a filter `l` over a type `α`, if a function `f` from `α` to `β` is nonnegative almost everywhere (i.e., everywhere except on a set of measure zero) with respect to the filter `l`, and if a function `g` from `α` to `β` tends towards infinity with respect to the filter `l`, then the function `(fun x => f x + g x)` that adds the values of `f` and `g` also tends towards infinity with respect to the filter `l`. This reflects the intuition that adding a nonnegative function to a function that tends to infinity should result in a function that also tends to infinity.
More concisely: If a non-negative function adds to a function tending to infinity almost everywhere with respect to a filter, then the sum also tends to infinity with respect to that filter.
|
Filter.Tendsto.neg_const_mul_atTop
theorem Filter.Tendsto.neg_const_mul_atTop :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α},
r < 0 → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => r * f x) l Filter.atBot
The theorem `Filter.Tendsto.neg_const_mul_atTop` states that for any types `α` and `β`, given a linearly ordered field structure on `α`, a filter `l` on `β`, a function `f` from `β` to `α`, and a constant `r` from `α` that is less than zero, if the function `f` tends to infinity (i.e., its limit is infinity) along the filter `l`, then the function obtained by multiplying `f` by `r` (i.e., the function `(fun x => r * f x)`) tends to negative infinity along the same filter `l`. In other words, multiplying a function by a negative constant reverses the direction of its growth towards infinity.
More concisely: If a function tends to infinity along a filter and a constant is less than zero, then the product of the function and the constant tends to negative infinity along the same filter.
|
Filter.extraction_of_frequently_atTop
theorem Filter.extraction_of_frequently_atTop :
∀ {P : ℕ → Prop}, (∃ᶠ (n : ℕ) in Filter.atTop, P n) → ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
The theorem `Filter.extraction_of_frequently_atTop` states that if a property `P` holds frequently at the limit towards infinity (`Filter.atTop`) for natural numbers, then there exists a strictly increasing function `φ` such that for every natural number `n`, the property `P` holds for `φ(n)`. In other words, we can extract a strictly increasing sequence of natural numbers where the property `P` is always true.
More concisely: If a property holds frequently at the limit towards infinity for natural numbers, then there exists a strictly increasing function mapping every natural number to a number where the property holds.
|
Filter.Tendsto.atTop_mul_const
theorem Filter.Tendsto.atTop_mul_const :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α},
0 < r → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x * r) l Filter.atTop
The theorem `Filter.Tendsto.atTop_mul_const` states that for any function `f` that tends towards infinity along a filter `l`, if `f` is multiplied by a positive constant `r`, then the resulting function also tends towards infinity along the same filter `l`. This theorem applies in the context of a linear ordered semifield, which is a mathematical structure that combines the properties of an ordered ring and a field, and allows operations such as addition, multiplication, and order comparison. If you are dealing with natural numbers or integers, you should use the variant `filter.tendsto.atTop_mul_const'`.
More concisely: If `f` tends towards infinity along filter `l` in a linear ordered semifield, then the function `x ↦ r * f(x)` also tends towards infinity along `l`, where `r` is a positive constant.
|
Filter.tendsto_div_const_atTop_iff_pos
theorem Filter.tendsto_div_const_atTop_iff_pos :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α}
[inst_1 : l.NeBot],
Filter.Tendsto f l Filter.atTop → (Filter.Tendsto (fun x => f x / r) l Filter.atTop ↔ 0 < r)
The theorem named `Filter.tendsto_div_const_atTop_iff_pos` states that for any types `α` and `β`, given a function `f` from `β` to `α`, a nontrivial filter `l` on `β`, and a value `r` of type `α`, under the condition that `α` is a linear ordered semifield and the filter `l` is non-empty, if the function `f` tends to infinity along the filter `l`, then the function `x ↦ f(x) / r` tends to infinity along `l` if and only if `r` is greater than zero.
In simpler terms, the theorem says that if a function's values grow indefinitely as we follow the filter `l`, then when we divide the output of this function by some positive number `r`, the resulting function will also grow indefinitely as we follow the filter `l`.
More concisely: If `α` is a linear ordered semifield and `l` is a non-empty filter on `β`, then for a function `f` from `β` to `α` and a positive `r` in `α`, `f` tends to infinity along `l` if and only if `f / r` tends to infinity along `l`.
|
Filter.mem_atTop_sets
theorem Filter.mem_atTop_sets :
∀ {α : Type u_3} [inst : Nonempty α] [inst : SemilatticeSup α] {s : Set α},
s ∈ Filter.atTop ↔ ∃ a, ∀ b ≥ a, b ∈ s
This theorem states that for any type `α` which is both nonempty and a semi-lattice with a supremum operation, and for any set `s` of elements of this type, `s` lies in the filter `atTop` (which represents the limit as we approach infinity on an ordered set) if and only if there exists an element `a` such that for all elements `b` that are greater than or equal to `a`, `b` is an element of `s`. In other words, a set `s` is in the filter `atTop` iff there is a point from which onwards all elements belong to `s`.
More concisely: For any nonempty type `α` with a supremum operation and any set `s` of elements from `α`, `s` lies in the filter `atTop` if and only if there exists an element `a` such that all elements greater than or equal to `a` are in `s`.
|
Filter.tendsto_mul_const_atTop_of_neg
theorem Filter.tendsto_mul_const_atTop_of_neg :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α},
r < 0 → (Filter.Tendsto (fun x => f x * r) l Filter.atTop ↔ Filter.Tendsto f l Filter.atBot)
The theorem `Filter.tendsto_mul_const_atTop_of_neg` states that for any types `α` and `β`, where `α` is a linearly ordered field, and for any filter `l` over `β`, any function `f` from `β` to `α`, and any real number `r` less than zero, the function `f` multiplied by `r` tends to infinity (represented by the filter `atTop`) as we move along the filter `l` if and only if the function `f` itself tends to negative infinity (represented by the filter `atBot`) along the same filter `l`. In other words, if a function goes to negative infinity as its input goes to a certain limit, then that function multiplied by a negative constant goes to positive infinity as the input goes to the same limit.
More concisely: For any linearly ordered field `α`, filter `l` over `β`, function `f` from `β` to `α`, and real number `r < 0`, `r * f` tends to `atTop` along `l` if and only if `f` tends to `atBot` along `l`.
|
Mathlib.Order.Filter.AtTopBot._auxLemma.27
theorem Mathlib.Order.Filter.AtTopBot._auxLemma.27 :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [inst_1 : l.NeBot],
Filter.Tendsto (fun x => r * f x) l Filter.atBot =
(0 < r ∧ Filter.Tendsto f l Filter.atBot ∨ r < 0 ∧ Filter.Tendsto f l Filter.atTop)
This theorem states that for any types `α` and `β`, with `α` being a linear ordered field, any filter `l` on `β` that is not bottom (i.e., not empty), any function `f` from `β` to `α`, and any real number `r`, the function that multiplies `r` with the output of `f` tends to negative infinity along the filter `l` if and only if either `r` is positive and `f` itself tends to negative infinity along `l`, or `r` is negative and `f` tends to positive infinity along `l`. In other words, the sign of `r` determines whether `f` should tend to positive or negative infinity for `r * f` to tend to negative infinity.
More concisely: For any linear ordered field `α`, filter `l` on type `β`, function `f` from `β` to `α`, and real number `r`, if `l` is non-empty and `r * f` tends to negative infinity along `l`, then either `r` is positive and `f` tends to negative infinity along `l`, or `r` is negative and `f` tends to positive infinity along `l`.
|
Filter.tendsto_const_mul_atBot_of_pos
theorem Filter.tendsto_const_mul_atBot_of_pos :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α},
0 < r → (Filter.Tendsto (fun x => r * f x) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot)
This theorem states that for any given positive constant `r`, a function `f` multiplied by `r` tends to negative infinity along a specific filter if and only if the original function `f` tends to negative infinity along the same filter. This holds for any types `α` and `β` where `α` is a linearly ordered field. The filter in this context represents a form of "limiting process" like converging to a particular value or tending to infinity. In this particular case, `Filter.atBot` represents the limit tending to negative infinity.
More concisely: For any positive constant `r` and linearly ordered field types `α`, if function `f` tends to negative infinity along filter `Filter.atBot`, then function `rf` (`r * f`) also tends to negative infinity along `Filter.atBot`. Conversely, if `rf` tends to negative infinity along `Filter.atBot`, then `f` also does.
|
Filter.mem_atTop
theorem Filter.mem_atTop : ∀ {α : Type u_3} [inst : Preorder α] (a : α), {b | a ≤ b} ∈ Filter.atTop
The theorem `Filter.mem_atTop` states that for any type `α` that is a preorder, and for any element `a` of type `α`, the set of all elements `b` such that `a` is less than or equal to `b` belongs to the filter that represents the limit tending to infinity on this set. In other words, the upper set `{b | a ≤ b}` is always in the top filter of the preorder.
More concisely: For any preorder type `α` and element `a` in `α`, the upper set `{b | a ≤ b}` is in the top filter of the preorder.
|
StrictMono.tendsto_atTop
theorem StrictMono.tendsto_atTop : ∀ {φ : ℕ → ℕ}, StrictMono φ → Filter.Tendsto φ Filter.atTop Filter.atTop
The theorem `StrictMono.tendsto_atTop` states that for any strictly monotone function `φ` from natural numbers to natural numbers, the function `φ` tends to infinity as its argument tends to infinity. In other words, if for every pair of natural numbers `a` and `b`, where `a < b`, it holds that `φ(a) < φ(b)`, then for every neighborhood of infinity in the codomain, the preimage under `φ` is a neighborhood of infinity in the domain.
More concisely: For any strictly monotonic function φ from natural numbers to natural numbers, if for all a < b, φ(a) < φ(b), then φ is unbounded.
|
Filter.tendsto_zpow_atTop_atTop
theorem Filter.tendsto_zpow_atTop_atTop :
∀ {α : Type u_3} [inst : LinearOrderedSemifield α] {n : ℤ},
0 < n → Filter.Tendsto (fun x => x ^ n) Filter.atTop Filter.atTop
This theorem states that for any type `α` which is a linear ordered semifield and for any integer `n` greater than 0, the function `f(x) = x^n` tends to infinity as `x` tends to infinity. In other words, as the input `x` becomes large without bound, the output `f(x)` also becomes large without bound. This is a formal way of expressing that the function `f(x) = x^n` exhibits a behavior of growing without bound as `x` grows without bound, for positive integer `n`.
More concisely: For any linear ordered semifield type `α` and positive integer `n`, the function `x ↦ x^n` approaches infinity as `x` approaches infinity.
|
Filter.Tendsto.eventually_ne_atTop
theorem Filter.Tendsto.eventually_ne_atTop :
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] [inst_1 : NoMaxOrder β] {f : α → β} {l : Filter α},
Filter.Tendsto f l Filter.atTop → ∀ (c : β), ∀ᶠ (x : α) in l, f x ≠ c
The theorem `Filter.Tendsto.eventually_ne_atTop` asserts that for any function `f` from a type `α` to a preorder type `β` with no maximum element, and any filter `l` on `α`, if `f` tends to positive infinity (`Filter.atTop`) along the filter `l`, then for every constant `c` in `β`, eventually in the filter `l`, the function `f(x)` is not equal to the constant `c`. In other words, if a function goes to infinity, then given any constant, there is a point beyond which the function value will not be equal to that constant.
More concisely: If a function from a type without a maximum element tends to positive infinity along a filter, then for any constant, there exists a filter element such that the function value at that element is not equal to the constant.
|
Filter.tendsto_const_mul_atBot_iff_pos
theorem Filter.tendsto_const_mul_atBot_iff_pos :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [inst_1 : l.NeBot],
Filter.Tendsto f l Filter.atBot → (Filter.Tendsto (fun x => r * f x) l Filter.atBot ↔ 0 < r)
The theorem `Filter.tendsto_const_mul_atBot_iff_pos` states that for any type `α` that is a linearly ordered field, a nontrivial filter `l` of type `β`, a function `f` from `β` to `α`, and a constant `r` of type `α`, if the function `f` tends to negative infinity along the filter `l`, then the new function defined as `r` times `f` also tends to negative infinity along the filter `l` if and only if `r` is greater than zero. In other words, multiplying a function that tends towards negative infinity by a positive constant results in a function that also tends towards negative infinity.
More concisely: For a linearly ordered field `α`, a nontrivial filter `l` over `β`, a function `f : β → α`, and a constant `r > 0` in `α`, if `f` tends to negative infinity along `l`, then the function `r * f` also tends to negative infinity along `l`.
|
Filter.Tendsto.atBot_mul_const
theorem Filter.Tendsto.atBot_mul_const :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α},
0 < r → Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => f x * r) l Filter.atBot
The theorem `Filter.Tendsto.atBot_mul_const` states that for any types `α` and `β`, where `α` is a linear ordered field, along with a filter `l` on `β`, a function `f` from `β` to `α` and a constant `r` from `α` such that `r` is greater than zero. If the function `f` tends to negative infinity (`Filter.atBot`) along the filter `l`, then the function `f` multiplied by the positive constant `r` (on the right) also tends to negative infinity along the filter `l`.
More concisely: If a function from a type equipped with a filter and the real numbers, where the function tends to negative infinity along the filter and the function's values are in a linear ordered field, then the function multiplied by a positive constant also tends to negative infinity along that filter.
|
Filter.atBot_Iic_eq
theorem Filter.atBot_Iic_eq :
∀ {α : Type u_3} [inst : SemilatticeInf α] (a : α), Filter.atBot = Filter.comap Subtype.val Filter.atBot
The theorem `Filter.atBot_Iic_eq` states that for any type `α` which is a semilattice with respect to an infimum operation (an operation that finds the greatest lower bound of a set), and any instance `a` of this type, the limit filter `atBot` (representing limit towards negative infinity) for the open interval `Set.Iic a` (the set of elements less than or equal to `a`) is derived from the `atBot` filter in the encompassing order. This is done by using the `Filter.comap` function together with the `Subtype.val` function, which returns the underlying element of a subtype. In other words, the behavior of the `atBot` filter in the specific context of an interval `Set.Iic a` mirrors its behavior in the larger order.
More concisely: The limit filter at the bottom element in an ordered semilattice is equal to the restriction of this filter to the open interval with this element as an upper bound.
|
Filter.eventually_ne_atTop
theorem Filter.eventually_ne_atTop :
∀ {α : Type u_3} [inst : Preorder α] [inst_1 : NoMaxOrder α] (a : α), ∀ᶠ (x : α) in Filter.atTop, x ≠ a
The theorem `Filter.eventually_ne_atTop` states that for any type `α` which has a preorder relation and does not have a maximum element (captured by the `NoMaxOrder α` instance), given any element `a` of type `α`, there will eventually be an element `x` such that `x ≠ a` as `x` approaches infinity (`x` is taken from the filter representing limit towards infinity, `Filter.atTop`). In other words, if we keep ascending in the order, we will eventually find elements different from `a`.
More concisely: For any type `α` without a maximum element in a preorder relation, there exists an element `x` in the filter of limit elements that is different from any given element `a`.
|
Filter.prod_atBot_atBot_eq
theorem Filter.prod_atBot_atBot_eq :
∀ {β₁ : Type u_6} {β₂ : Type u_7} [inst : Preorder β₁] [inst_1 : Preorder β₂],
Filter.atBot ×ˢ Filter.atBot = Filter.atBot
This theorem states that for any two types `β₁` and `β₂` that have preorder relationships, the product of filters `atBot` (which represents the limit towards negative infinity on an ordered set) over both types is the same as the `atBot` filter. In mathematical terms, this means that the limit as both variables approach negative infinity in a Cartesian product space of two preordered sets is the same as the limit as a single variable approaches negative infinity in a single preordered set.
More concisely: For any preordered types `β₁` and `β₂`, the filter of limits towards negative infinity on their product equals the filter of limits towards negative infinity on each type.
|
Filter.tendsto_of_subseq_tendsto
theorem Filter.tendsto_of_subseq_tendsto :
∀ {α : Type u_6} {ι : Type u_7} {x : ι → α} {f : Filter α} {l : Filter ι} [inst : l.IsCountablyGenerated],
(∀ (ns : ℕ → ι),
Filter.Tendsto ns Filter.atTop l → ∃ ms, Filter.Tendsto (fun n => x (ns (ms n))) Filter.atTop f) →
Filter.Tendsto x l f
The theorem `Filter.tendsto_of_subseq_tendsto` states that for a sequence `x` over any types `α` and `ι`, if every subsequence `ns` of `x` converging to a filter `l` has a subsequence `ms` such that the sequence obtained by applying `x` to the terms of `ms` converges to a filter `f`, then the original sequence `x` also converges to the filter `f`. Here, the convergence of a sequence to a filter is defined in terms of the `Filter.Tendsto` predicate, which says that for every neighborhood of the limit defined by the filter, the pre-image of that neighborhood under the sequence is eventually always in that neighborhood. The filter `l` is assumed to be countably generated. The filter `atTop` represents the limit towards infinity, and is involved in defining the convergence of the subsequences.
More concisely: If every convergent subsequence of a sequence `x` over `α` and `ι` has a further convergent subsequence `ms` such that `x` applied to `ms` converges to a filter `f`, and `l` is a countably generated filter over `α` such that every convergent subsequence of `x` converges to `l`, then `x` converges to `f`.
|
Filter.tendsto_neg_atTop_atBot
theorem Filter.tendsto_neg_atTop_atBot :
∀ {β : Type u_4} [inst : OrderedAddCommGroup β], Filter.Tendsto Neg.neg Filter.atTop Filter.atBot
The theorem `Filter.tendsto_neg_atTop_atBot` states that for any type `β` that forms an ordered additive commutative group, the function that maps each element to its negation (denoted by `Neg.neg`) tends to negative infinity (`Filter.atBot`) as the input tends to positive infinity (`Filter.atTop`). In other words, as we take larger and larger values in this group, their negatives become smaller and smaller, approaching negative infinity.
More concisely: For any ordered additive commutative group type `β`, the function `Neg.neg` tends to `Filter.atBot` as elements approach `Filter.atTop`.
|
Filter.tendsto_mul_const_atBot_iff_neg
theorem Filter.tendsto_mul_const_atBot_iff_neg :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [inst_1 : l.NeBot],
Filter.Tendsto f l Filter.atTop → (Filter.Tendsto (fun x => f x * r) l Filter.atBot ↔ r < 0)
The theorem `Filter.tendsto_mul_const_atBot_iff_neg` states that for any types `α` and `β`, where `α` is a linearly ordered field, and for any nontrivial filter `l` over `β` and any function `f` from `β` to `α` and any real number `r`, if `f` tends to infinity along the filter `l`, then the function `x ↦ f(x) * r` tends to negative infinity along the same filter if and only if `r` is less than zero. The filter `l` is said to be nontrivial, represented as `l.NeBot`, meaning that it is not the bottom filter which contains all sets. The function `f` tending to infinity is represented as `Filter.Tendsto f l Filter.atTop`, where `Filter.atTop` is the filter representing the limit toward infinity. Similarly, the function `x ↦ f(x) * r` tending to negative infinity is represented as `Filter.Tendsto (fun x => f x * r) l Filter.atBot`, where `Filter.atBot` is the filter representing the limit toward negative infinity.
More concisely: For a linearly ordered field `α`, nontrivial filter `l` over `β`, function `f` from `β` to `α`, and real number `r`, `Filter.Tendsto f l Filter.atTop` and `Filter.Tendsto (fun x => f x * r) l Filter.atBot` are equivalent if and only if `r` is negative.
|
Filter.tendsto_iff_seq_tendsto
theorem Filter.tendsto_iff_seq_tendsto :
∀ {α : Type u_3} {β : Type u_4} {f : α → β} {k : Filter α} {l : Filter β} [inst : k.IsCountablyGenerated],
Filter.Tendsto f k l ↔ ∀ (x : ℕ → α), Filter.Tendsto x Filter.atTop k → Filter.Tendsto (f ∘ x) Filter.atTop l
This theorem provides an abstract version of the concept of continuity for sequentially continuous functions on metric spaces. Specifically, it states that for any function `f` mapping from type `α` to `β`, a filter `k` on `α`, and a filter `l` on `β`, if the filter `k` is countably generated, then the function `f` tends to filter `l` given the input filter `k` if and only if for every sequence `x` (mapping from natural numbers to `α`) that tends to filter `k` as its index goes to infinity, the sequence resulting from applying the function `f` on `x` (denoted as `f ∘ x`) also tends to filter `l` as its index goes to infinity. In other words, under these conditions, `f` preserves the sequential convergence properties of sequences.
More concisely: A sequentially continuous function on a metric space preserves the sequential convergence of filters: if a filter on the domain is countably generated and a sequence in the filter converges to a filter on the codomain, then the image sequence of the function converges to that filter.
|
Filter.tendsto_atTop_atTop
theorem Filter.tendsto_atTop_atTop :
∀ {α : Type u_3} {β : Type u_4} [inst : Nonempty α] [inst : SemilatticeSup α] [inst_1 : Preorder β] {f : α → β},
Filter.Tendsto f Filter.atTop Filter.atTop ↔ ∀ (b : β), ∃ i, ∀ (a : α), i ≤ a → b ≤ f a
The theorem `Filter.tendsto_atTop_atTop` states that for a function `f` from an ordered set `α` to an ordered set `β`, the function `f` has the property of tending to positive infinity if and only if for any element `b` from `β`, there exists an element `i` in `α` such that for all elements `a` in `α` which are greater than or equal to `i`, `f(a)` is greater than or equal to `b`. Note that `α` is a set with a least upper bound (a semilattice) and `β` is simply a preordered set. This essentially means that the function `f` grows to `+∞` irrespective of the order-preserving nature of an embedding function `e`.
More concisely: A function from an ordered set to another preordered set tends to positive infinity if and only if for every element in the range, there exists an element in the domain that maps to a value greater than or equal to it. (Assuming the domain has a least upper bound.)
|
Filter.tendsto_finset_range
theorem Filter.tendsto_finset_range : Filter.Tendsto Finset.range Filter.atTop Filter.atTop
The theorem `Filter.tendsto_finset_range` states that the function `Finset.range` tends to infinity, as defined by the `Filter.atTop` filter, when its input tends to infinity. In other words, as the input natural number increases without bound, the set of natural numbers less than that input, which is generated by the `Finset.range` function, also increases without bound. This is a formal way to express the intuitive notion that the range of a number, or the set of all natural numbers less than it, grows as the number itself grows.
More concisely: The `Finset.range` function maps larger natural numbers to larger and unbounded finite sets.
|
Filter.tendsto_atTop_of_monotone_of_filter
theorem Filter.tendsto_atTop_of_monotone_of_filter :
∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder ι] [inst_1 : Preorder α] {l : Filter ι} {u : ι → α},
Monotone u → ∀ [inst_2 : l.NeBot], Filter.Tendsto u l Filter.atTop → Filter.Tendsto u Filter.atTop Filter.atTop
The theorem states that for any monotonically increasing function `u` from a preorder type `ι` to another preorder type `α`, if `u` tends to infinity (represented by `atTop`) along any non-trivial filter `l`, then `u` also tends to infinity along `atTop`. In other words, if for any given value in `α`, there is a point in the domain after which `u` always produces higher values, and this holds for values defined by some non-empty filter `l`, then this property also holds for the whole domain.
More concisely: If `u` is a monotonically increasing function from a preorder type `ι` to another preorder type `α` and `u` tends to infinity along any non-trivial filter `l` in `ι`, then `u` tends to infinity at the top element of `ι`.
|
Filter.tendsto_mul_const_atTop_iff
theorem Filter.tendsto_mul_const_atTop_iff :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [inst_1 : l.NeBot],
Filter.Tendsto (fun x => f x * r) l Filter.atTop ↔
0 < r ∧ Filter.Tendsto f l Filter.atTop ∨ r < 0 ∧ Filter.Tendsto f l Filter.atBot
The theorem `Filter.tendsto_mul_const_atTop_iff` states that for a nontrivial filter `l`, a function `f` from `β` to a linearly ordered field `α`, and a real number `r`, the function `f` multiplied by `r` tends to infinity along the filter `l` if and only if either `r` is greater than zero and `f` tends to infinity along `l`, or `r` is less than zero and `f` tends to negative infinity along `l`. In other words, the direction in which the function `f*r` tends towards depends on the sign of `r` and the limit of `f` along the filter `l`.
More concisely: For a nontrivial filter `l` on a linearly ordered field, a function `f` from a set `β` to the field, and a real number `r`, the function `f * r` tends to infinity along `l` if and only if either `r` is positive and `f` tends to infinity along `l`, or `r` is negative and `f` tends to negative infinity along `l`.
|
Filter.atTop_basis_Ioi
theorem Filter.atTop_basis_Ioi :
∀ {α : Type u_3} [inst : Nonempty α] [inst : SemilatticeSup α] [inst_1 : NoMaxOrder α],
Filter.atTop.HasBasis (fun x => True) Set.Ioi
The theorem `Filter.atTop_basis_Ioi` states that for any type `α` which is nonempty, has a sup-semilattice structure, and has no maximum element, the filter `Filter.atTop` (representing the limit towards positive infinity) has a basis constructed by the collection of all sets of the form `Set.Ioi x` (the open interval from `x` to positive infinity) for all `x` in `α`. In essence, this means that 'going to infinity' in this ordered set can be characterized by 'passing all elements' of the set.
More concisely: For a nonempty, sup-semilatticed, and boundless type `α`, `Filter.atTop` has a basis consisting of all open intervals `( Set.Ioi x : α)`.
|
Filter.map_val_atTop_of_Ici_subset
theorem Filter.map_val_atTop_of_Ici_subset :
∀ {α : Type u_3} [inst : SemilatticeSup α] {a : α} {s : Set α},
Set.Ici a ⊆ s → Filter.map Subtype.val Filter.atTop = Filter.atTop
This theorem states that for any type `α` under a semilattice with supremum, given any element `a` of that type and any set `s` of elements of that type, if the set of all elements greater or equal to `a` (denoted as `Set.Ici a`) is a subset of `s`, then the forward map `Filter.map` of the filter `Filter.atTop` (representing limit at infinity) using the `Subtype.val` function (which yields the underlying element of a subtype) equals the filter at infinity `Filter.atTop`. This essentially means that under the given conditions, mapping the elements of the filter at infinity using `Subtype.val` does not affect the filter.
More concisely: For any semilattice with supremum `α`, if `a` is an element of `α` and `Set.Ici a ⊆ s`, then `Filter.map Filter.atTop Subtype.val = Filter.atTop` for filters on the set `s` of elements of `α`.
|
Filter.mem_atBot_sets
theorem Filter.mem_atBot_sets :
∀ {α : Type u_3} [inst : Nonempty α] [inst : SemilatticeInf α] {s : Set α},
s ∈ Filter.atBot ↔ ∃ a, ∀ b ≤ a, b ∈ s
The theorem `Filter.mem_atBot_sets` states that for any nonempty set `s` of elements of a type `α`, where `α` is equipped with an infimum operation (forming a semilattice), `s` is in the filter `atBot` (representing the limit towards negative infinity in an ordered set) if and only if there exists an element `a` in `α` such that every element `b` less than or equal to `a` is in `s`. In simpler terms, a set is approaching negative infinity if there exists a boundary such that all elements beneath this boundary are within the set.
More concisely: A nonempty set `s` of an infimum-closed type `α` is in the filter of elements approaching negative infinity if and only if it contains an element `a` such that every element less than or equal to `a` is in `s`.
|
OrderIso.comap_atTop
theorem OrderIso.comap_atTop :
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β),
Filter.comap (⇑e) Filter.atTop = Filter.atTop
The theorem `OrderIso.comap_atTop` states that for any two preordered types `α` and `β` and an order isomorphism `e` between them, the preimage (or inverse image) under `e` of the filter representing the limit towards infinity in `β` is the filter representing the limit towards infinity in `α`. In other words, pulling back the "towards infinity" filter along an order isomorphism doesn't change the filter.
More concisely: For any order isomorphism between preordered types `α` and `β`, the inverse image of the filter of limit points in `β` is the filter of limit points in `α`.
|
Filter.tendsto_add_atTop_iff_nat
theorem Filter.tendsto_add_atTop_iff_nat :
∀ {α : Type u_3} {f : ℕ → α} {l : Filter α} (k : ℕ),
Filter.Tendsto (fun n => f (n + k)) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l
The theorem `Filter.tendsto_add_atTop_iff_nat` states that for any type `α`, any function `f` from natural numbers to `α`, any filter `l` on `α`, and any natural number `k`, the function `f` tends to `l` as its argument tends to infinity if and only if the function `f` composed with the addition of `k` also tends to `l` as its argument tends to infinity. In other words, adding a constant `k` to the argument of `f` does not change the limiting behavior of the function as the argument approaches infinity.
More concisely: For any type α, function f from natural numbers to α, filter l on α, and natural number k, the function f tends to l as its argument tends to infinity if and only if the function f composed with the constant function adding k also tends to l as its argument tends to infinity.
|
Monotone.tendsto_atBot_atBot
theorem Monotone.tendsto_atBot_atBot :
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Monotone f → (∀ (b : β), ∃ a, f a ≤ b) → Filter.Tendsto f Filter.atBot Filter.atBot
The theorem `Monotone.tendsto_atBot_atBot` states that for any types `α` and `β` that have a preorder, and any function `f` from `α` to `β`, if `f` is monotone and for every element `b` in `β`, there exists an element `a` in `α` such that `f(a)` is less than or equal to `b`, then the function `f` tends to negative infinity at negative infinity. In other words, as we move towards smaller and smaller values in `α`, the values of `f` also trend towards smaller and smaller values.
More concisely: If `α` and `β` are preordered types, `f` is a monotone function from `α` to `β`, and for every `b` in `β`, there exists an `a` in `α` with `f(a) ≤ b`, then `f` tends to negative infinity as inputs in `α` approach negative infinity.
|
Filter.prod_atTop_atTop_eq
theorem Filter.prod_atTop_atTop_eq :
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β],
Filter.atTop ×ˢ Filter.atTop = Filter.atTop
The theorem `Filter.prod_atTop_atTop_eq` states that for any two types `α` and `β` that have a preorder (a reflexive and transitive binary relation), the product filter of `Filter.atTop` for `α` and `Filter.atTop` for `β` is equal to `Filter.atTop`. In other words, the limit towards infinity of the product of two ordered sets is the same as the limit towards infinity of the individual sets.
More concisely: For preordered types `α` and `β`, the product filter of `Filter.atTop` for `α` and `Filter.atTop` for `β` equals `Filter.atTop`.
|
Filter.map_atTop_eq_of_gc
theorem Filter.map_atTop_eq_of_gc :
∀ {α : Type u_3} {β : Type u_4} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {f : α → β} (g : β → α)
(b' : β),
Monotone f →
(∀ (a : α), ∀ b ≥ b', f a ≤ b ↔ a ≤ g b) → (∀ b ≥ b', b ≤ f (g b)) → Filter.map f Filter.atTop = Filter.atTop
The theorem `Filter.map_atTop_eq_of_gc` states that for any two types `α` and `β` with a `SemilatticeSup` structure (a type of order where every two elements have a least upper bound), a function `f` from `α` to `β`, and its right inverse `g` from `β` to `α`, and a value `b'` of type `β`, if `f` is monotone (i.e., it preserves the order), and for all `a` of type `α` and `b` of type `β` greater than or equal to `b'`, `f a` is less than or equal to `b` if and only if `a` is less than or equal to `g b`, and for all `b` greater than or equal to `b'`, `b` is less than or equal to `f (g b)`, then the forward image of the filter `atTop` (which represents the limit as `α` approaches infinity) under `f` is also `atTop`. This theorem essentially tells us that a monotone function under certain conditions preserves the property of approaching infinity.
More concisely: If `f : α → β` is a monotone function between semilattices with right inverse `g` such that for all `b' ∈ β` and `a ∈ α`, `f a ≤ b` if and only if `a ≤ g b` and for all `b ≥ b'`, `b ≤ f (g b)`, then `f''(Filter.atTop α) = Filter.atTop β`.
|
Filter.tendsto_atTop'
theorem Filter.tendsto_atTop' :
∀ {α : Type u_3} {β : Type u_4} [inst : Nonempty α] [inst : SemilatticeSup α] {f : α → β} {l : Filter β},
Filter.Tendsto f Filter.atTop l ↔ ∀ s ∈ l, ∃ a, ∀ b ≥ a, f b ∈ s
The theorem `Filter.tendsto_atTop'` states that for any types `α` and `β`, given `α` is nonempty and a semilattice with supremum, a function `f` from `α` to `β`, and a filter `l` on `β`, the function `f` has the property of `Filter.Tendsto` with respect to the filter `Filter.atTop` on `α` and the filter `l` on `β` if and only if for every set `s` in the filter `l`, there exists an element `a` in `α` such that for all `b` in `α` greater than or equal to `a`, the image of `b` under `f` is in `s`. In simpler terms, `f` approaches a limit in the filter `l` as the input approaches infinity if and only if for every set around the limit, we can find a threshold beyond which the function's values are always within that set.
More concisely: For a function from a nonempty semilattice with supremum to another type, the function tends to a limit in a filter if and only if for every set in the filter, there exists an element such that the images of all larger elements are contained in the set.
|
Filter.Tendsto.atTop_div_const
theorem Filter.Tendsto.atTop_div_const :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α},
0 < r → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x / r) l Filter.atTop
The theorem `Filter.Tendsto.atTop_div_const` states that for any function `f` mapping from type `β` to a linearly ordered semifield `α`, if the function `f` tends towards infinity with respect to a given filter `l`, then the function `f` divided by any positive constant `r` also tends towards infinity along the same filter `l`. In other words, if `f(x)` goes to infinity as `x` approaches some value according to the filter `l`, then `f(x)/r` will also go to infinity, provided `r` is a positive constant.
More concisely: If a function `f : β → α` tends towards infinity along a filter `l` and `r` is a positive constant, then `f / r` also tends towards infinity along `l`.
|
Filter.tendsto_mul_const_atBot_of_neg
theorem Filter.tendsto_mul_const_atBot_of_neg :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α},
r < 0 → (Filter.Tendsto (fun x => f x * r) l Filter.atBot ↔ Filter.Tendsto f l Filter.atTop)
The theorem `Filter.tendsto_mul_const_atBot_of_neg` states that for any types `α` and `β`, where `α` is a linear ordered field, any filter `l` of type `β`, any function `f` mapping `β` to `α`, and any real number `r` that is less than zero, the function `f` multiplied by `r` tends to negative infinity along the filter `l` if and only if `f` itself tends to positive infinity along `l`. In other words, if we have a function that tends towards positive infinity, and we multiply it by a negative constant, the resulting function will tend towards negative infinity.
More concisely: For any linear ordered field `α`, filter `l` over type `β`, function `f : β → α`, and real number `r < 0`, if `f` tends to +∞ along `l`, then `rf` tends to -∞ along `l`.
|
Filter.exists_seq_forall_of_frequently
theorem Filter.exists_seq_forall_of_frequently :
∀ {ι : Type u_6} {l : Filter ι} {p : ι → Prop} [inst : l.IsCountablyGenerated],
(∃ᶠ (n : ι) in l, p n) → ∃ ns, Filter.Tendsto ns Filter.atTop l ∧ ∀ (n : ℕ), p (ns n)
The theorem `Filter.exists_seq_forall_of_frequently` states that for any type `ι`, a filter `l` on `ι`, and a predicate `p` on `ι`, if the filter `l` is countably generated, and there frequently exist `ι` in the filter `l` that satisfy the predicate `p`, then there exists a sequence `ns` that tends from positive infinity to `l` and for every natural number `n`, `p` is true for `ns n`.
In other words, if `p` is frequently true for elements in a countably generated filter, there exists a sequence with values in the filter such that `p` is true for all elements of the sequence. This sequence can be thought of as drawing from the infinitely occurring elements in the filter for which `p` holds. The "tending to `l`" part ensures that this sequence is drawing from elements that are increasingly deep into the filter.
More concisely: If `ι` is a type, `l` is a countably generated filter on `ι`, and `p` is a predicate on `ι` such that `p` frequently holds in `l`, then there exists a sequence `ns` in `l` such that `p(ns n)` holds for all natural numbers `n`.
|
Filter.atTop_basis
theorem Filter.atTop_basis :
∀ {α : Type u_3} [inst : Nonempty α] [inst : SemilatticeSup α], Filter.atTop.HasBasis (fun x => True) Set.Ici := by
sorry
The theorem `Filter.atTop_basis` states that for any type `α`, given that `α` is nonempty and forms a semilattice with respect to an operation `sup` (which stands for supremum), the filter `Filter.atTop` (representing the limit towards positive infinity in an ordered set) has a basis specified by the predicate function which always returns `True` and the set function `Set.Ici`. `Set.Ici` produces left-closed right-infinite intervals. In other words, this theorem asserts that the filter representing the limit towards positive infinity in a semilattice can be generated by considering all intervals of the form `[a, ∞)`, irrespective of the value of `a`.
More concisely: The filter `Filter.atTop` on a nonempty semilattice `α` with supremum operation `sup` has a basis consisting of all left-closed, right-infinite intervals `[a, ∞)`.
|
Filter.tendsto_atTop_mono'
theorem Filter.tendsto_atTop_mono' :
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] (l : Filter α) ⦃f₁ f₂ : α → β⦄,
l.EventuallyLE f₁ f₂ → Filter.Tendsto f₁ l Filter.atTop → Filter.Tendsto f₂ l Filter.atTop
The theorem `Filter.tendsto_atTop_mono'` states that, given an arbitrary filter `l` and two functions `f₁` and `f₂` from the type `α` to an ordered type `β`, if `f₁` is almost everywhere less than or equal to `f₂` with respect to the filter `l`, and if the function `f₁` tends to infinity (`Filter.atTop`) as the filter `l` tends to infinity, then the function `f₂` also tends to infinity as the filter `l` tends to infinity. This theorem essentially says that if `f₁` is smaller or equal to `f₂` and `f₁` tends to infinity, then `f₂` must also tend to infinity.
More concisely: If a filter converges to infinity for a function `f_1` that is pointwise less than or equal to another function `f_2`, then `f_2` also converges to infinity with respect to that filter.
|
Filter.map_val_Iio_atBot
theorem Filter.map_val_Iio_atBot :
∀ {α : Type u_3} [inst : SemilatticeInf α] [inst_1 : NoMinOrder α] (a : α),
Filter.map Subtype.val Filter.atBot = Filter.atBot
The theorem `Filter.map_val_Iio_atBot` states that for any type `α` with a `SemilatticeInf` structure (a partially ordered set where any two elements have a greatest lower bound) and a `NoMinOrder` structure (a densely ordered set without a least element), and for any element `a` of type `α`, mapping the underlying elements of the elements of the `atBot` filter (which represents the limit going to negative infinity) in the subtype of `α` to `α` itself (using the `Subtype.val` function) results in the `atBot` filter in `α`. In other words, the `atBot` filter for an open interval `Iio a` (all elements less than `a`) is derived from the `atBot` filter in the overall order `α`.
More concisely: For any type `α` equipped with both a `SemilatticeInf` and `NoMinOrder` structure, the mapping `Filter.map Filters.atBot (λ x => Subtype.val x)` results in the filter `Filters.atBot` in the subtype of `α` with respect to the suborder induced by the order on `α`.
|
Monotone.tendsto_atBot_atBot_iff
theorem Monotone.tendsto_atBot_atBot_iff :
∀ {α : Type u_3} {β : Type u_4} [inst : Nonempty α] [inst : SemilatticeInf α] [inst_1 : Preorder β] {f : α → β},
Monotone f → (Filter.Tendsto f Filter.atBot Filter.atBot ↔ ∀ (b : β), ∃ a, f a ≤ b)
The theorem `Monotone.tendsto_atBot_atBot_iff` states that for any type `α` which is nonempty, a semilattice with infimum, and another type `β` which is a preorder, and a given function `f` from `α` to `β`, if `f` is monotone, then `f` tends to `-∞` at `-∞` (i.e., `Filter.Tendsto f Filter.atBot Filter.atBot`) if and only if for every `b` in `β`, there exists an `a` in `α` such that `f(a)` is less than or equal to `b`. In other words, a monotone function's values get arbitrarily small as its argument gets arbitrarily small, if for every limit point, there exists an input that maps to a value not greater than that limit point.
More concisely: A monotone function from a nonempty semilattice with infimum to a preorder tends to negative infinity at negative infinity if and only if for every element in the preorder, there exists an element in the semilattice mapping to a value less than or equal to it.
|
Mathlib.Order.Filter.AtTopBot._auxLemma.4
theorem Mathlib.Order.Filter.AtTopBot._auxLemma.4 :
∀ {α : Type u_3} [inst : SemilatticeSup α] [inst_1 : Nonempty α] {p : α → Prop},
(∀ᶠ (x : α) in Filter.atTop, p x) = ∃ a, ∀ b ≥ a, p b
The theorem `Mathlib.Order.Filter.AtTopBot._auxLemma.4` states that for any type `α` equipped with a semilattice sup (an algebraic structure with a binary operation that is associative, commutative, and idempotent) and known to be nonempty, and for any property `p` on elements of `α`, the property `p` holds eventually at the limit towards infinity (`Filter.atTop`) if and only if there exists an element `a` in `α` such that `p` holds for all elements `b` greater or equal to `a`.
More concisely: For any semilattice `α` with a nonempty sup-domain and property `p` on `α`, `p` holds eventually at the limit towards infinity if and only if there exists an element `a` such that `p(b)` holds for all `b ≥ a`.
|
Filter.exists_lt_of_tendsto_atTop
theorem Filter.exists_lt_of_tendsto_atTop :
∀ {α : Type u_3} {β : Type u_4} [inst : SemilatticeSup α] [inst_1 : Preorder β] [inst_2 : NoMaxOrder β] {u : α → β},
Filter.Tendsto u Filter.atTop Filter.atTop → ∀ (a : α) (b : β), ∃ a' ≥ a, b < u a'
The theorem `Filter.exists_lt_of_tendsto_atTop` states that for any function `u` from a type `α` with a semilattice sup structure to a type `β` with a preorder structure and no maximum element, if the function `u` tends to infinity as the input tends to infinity (captured by `Filter.Tendsto u Filter.atTop Filter.atTop`), then for any elements `a` in `α` and `b` in `β`, there exists an element `a'` in `α` such that `a'` is greater than or equal to `a` and `u(a')` is strictly greater than `b`. In other words, if a function tends towards infinity as its input grows, you can always find a large enough input value such that the function value at that input point exceeds any given target.
More concisely: For any function from a semilattice without a maximum element to a preorder without a maximum element that tends to infinity, there exists an input element greater than any given input such that the function value at the larger input strictly exceeds the given output.
|
Filter.tendsto_add_atTop_nat
theorem Filter.tendsto_add_atTop_nat : ∀ (k : ℕ), Filter.Tendsto (fun a => a + k) Filter.atTop Filter.atTop
This theorem, `Filter.tendsto_add_atTop_nat`, states that for any natural number `k`, the function which adds `k` to its input tends towards infinity along with its input. In other words, if we take any sequence of natural numbers that goes to infinity and add `k` to every number in that sequence, the resulting sequence also goes to infinity. In mathematical terms, this can be expressed as $\lim_{n \to \infty} (n+k) = \infty$ for all natural numbers `k`.
More concisely: For all natural numbers `k`, the sequence `x => x + k` tends to infinity along with any sequence `x` that goes to infinity. (Mathematically, for all increasing sequences `{x_n}`, `lim (n : ℕ) (x_n + k) = ∞`. In Lean, this theorem is named `Filter.tendsto_add_atTop_nat`.)
|
OrderIso.map_atTop
theorem OrderIso.map_atTop :
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β),
Filter.map (⇑e) Filter.atTop = Filter.atTop
This theorem states that for any two preordered types `α` and `β`, and any order isomorphism `e` between `α` and `β`, the application of the forward map `Filter.map` of the order isomorphism `e` to the filter `Filter.atTop` of `α` results in the filter `Filter.atTop` of `β`. In other words, mapping the filter representing the limit towards infinity (`Filter.atTop`) in the preordered type `α` using the order isomorphism `e` gives us the filter representing the limit towards infinity in the preordered type `β`. This essentially means that the concept of 'going towards infinity' remains invariant under an order isomorphism.
More concisely: Given any order isomorphism between preordered types `α` and `β`, the image of the filter `Filter.atTop` of `α` under the forward map of the order isomorphism is equal to the filter `Filter.atTop` of `β`.
|
Filter.exists_seq_monotone_tendsto_atTop_atTop
theorem Filter.exists_seq_monotone_tendsto_atTop_atTop :
∀ (α : Type u_6) [inst : SemilatticeSup α] [inst_1 : Nonempty α] [inst_2 : Filter.atTop.IsCountablyGenerated],
∃ xs, Monotone xs ∧ Filter.Tendsto xs Filter.atTop Filter.atTop
This theorem states that for every type `α` which is a semilattice with a supremum operation, is nonempty, and has a filter `atTop` which is countably generated, there exists a sequence `xs` which is monotone (meaning that if an element `a` is less than or equal to `b`, then `xs a` is less than or equal to `xs b`) and tends to infinity along with the `atTop` filter. In other words, for every neighborhood of infinity in the `atTop` filter, the pre-image of that neighborhood under the `xs` sequence is also a neighborhood of infinity.
More concisely: For every nonempty semilattice `α` with a countably generated filter `atTop` and a supremum operation, there exists a monotone sequence `xs` such that for every neighborhood of infinity in `atTop`, `xs⁻¹(U)` is also a neighborhood of infinity.
|
Filter.Iic_mem_atBot
theorem Filter.Iic_mem_atBot : ∀ {α : Type u_3} [inst : Preorder α] (a : α), Set.Iic a ∈ Filter.atBot
This theorem states that for any type `α` with a preorder relationship, and for any element `a` of type `α`, the set of all elements `x` such that `x ≤ a` (`Set.Iic a`) is a member of the filter representing the limit towards negative infinity (`Filter.atBot`). Essentially, this theorem confirms that the set of all elements less than or equal to a given element is a valid down-set in the filter representing the concept of "going to negative infinity".
More concisely: For any type `α` with a preorder relation and any element `a` in `α`, the down-set `{x : α | x ≤ a}` belongs to the filter `Filter.atBot` of elements approaching the bottom element.
|
Filter.disjoint_atBot_atTop
theorem Filter.disjoint_atBot_atTop :
∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : Nontrivial α], Disjoint Filter.atBot Filter.atTop
The theorem `Filter.disjoint_atBot_atTop` states that for any non-trivial partially ordered type `α`, the filters `Filter.atBot` and `Filter.atTop` are disjoint. In other words, there is no element in `α` that is both arbitrarily close to negative infinity (`Filter.atBot`) and positive infinity (`Filter.atTop`) at the same time. Disjointness of filters here is defined as their infimum being the bottom element of the set, which generalizes the concept of disjoint sets.
More concisely: For any non-trivial partially ordered type `α`, the filters `Filter.atBot` and `Filter.atTop` have no common elements.
|
Filter.tendsto_neg_atBot_atTop
theorem Filter.tendsto_neg_atBot_atTop :
∀ {β : Type u_4} [inst : OrderedAddCommGroup β], Filter.Tendsto Neg.neg Filter.atBot Filter.atTop
The theorem `Filter.tendsto_neg_atBot_atTop` states that for any ordered additive commutative group `β`, the function that produces the negative of an element (`Neg.neg`) tends to infinity (`Filter.atTop`) as the input tends to negative infinity (`Filter.atBot`). In simpler terms, it says that as we go towards negative infinity in the group, flipping the sign of the elements will get us closer and closer to positive infinity.
More concisely: For any ordered additive commutative group β, the function Neg.neg is infinitely increasing as we approach negative infinity.
|
Filter.low_scores
theorem Filter.low_scores :
∀ {β : Type u_4} [inst : LinearOrder β] [inst_1 : NoMinOrder β] {u : ℕ → β},
Filter.Tendsto u Filter.atTop Filter.atBot → ∀ (N : ℕ), ∃ n ≥ N, ∀ k < n, u n < u k
The theorem `Filter.low_scores` states that for any sequence `u` of type `β` which is unbounded below (as indicated by `β` being a `LinearOrder` and having `NoMinOrder`), if the limit of `u` as `n` goes to infinity (`Filter.atTop`) is negative infinity (`Filter.atBot`), then for any natural number `N`, there exists a number `n` greater than or equal to `N` such that for all numbers `k` less than `n`, the `n`-th term of the sequence `u` is strictly less than the `k`-th term. In other words, if a sequence tends towards negative infinity, then after a certain point, the sequence hits a value that is strictly lower than all previous values.
More concisely: For any unbounded below sequence `u` of type `β` in a Linear Order with NoMinOrder, if the limit of `u` as `n` approaches infinity is negative infinity, then there exists an `N` such that for all `k` < `N`, `u(n)` < `u(k)`.
|
Filter.tendsto_const_mul_atBot_iff_neg
theorem Filter.tendsto_const_mul_atBot_iff_neg :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [inst_1 : l.NeBot],
Filter.Tendsto f l Filter.atTop → (Filter.Tendsto (fun x => r * f x) l Filter.atBot ↔ r < 0)
The theorem `Filter.tendsto_const_mul_atBot_iff_neg` states that for any non-trivial filter `l`, any function `f` from an arbitrary type `β` to a linearly ordered field `α`, and any element `r` of `α`, if `f` tends to infinity along `l` (that is, for every neighborhood of infinity in `α`, the preimage under `f` of that neighborhood is a neighborhood in `l`), then the function `g` defined by `g(x) = r * f(x)` tends to negative infinity along `l` if and only if `r` is less than zero. This means that multiplying `f` by a negative scalar causes it to flip from tending towards infinity to tending towards negative infinity.
More concisely: For a non-trivial filter `l` on a type, a function `f` from an arbitrary type to a linearly ordered field, and an element `r` of `α` with `r < 0`, if `f` tends to infinity along `l`, then `r * f` tends to negative infinity along `l`.
|
Filter.tendsto_div_const_atTop_of_pos
theorem Filter.tendsto_div_const_atTop_of_pos :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α},
0 < r → (Filter.Tendsto (fun x => f x / r) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop)
The theorem `Filter.tendsto_div_const_atTop_of_pos` states that for any types `α` and `β`, given a linear ordered semifield on `α`, a filter `l` on `β`, a function `f` from `β` to `α`, and a positive constant `r` in `α`, the function `f` divided by `r` tends to infinity along the filter `l` if and only if `f` itself tends to infinity along the same filter `l`. In other words, dividing a function by a positive constant does not affect its limit behavior towards infinity.
More concisely: For any linear ordered semifields `α`, types `β`, filters `l` on `β`, functions `f` from `β` to `α`, and positive constants `r` in `α`, if `f` tends to infinity along filter `l`, then `f / r` also tends to infinity along filter `l`.
|
Filter.exists_le_of_tendsto_atTop
theorem Filter.exists_le_of_tendsto_atTop :
∀ {α : Type u_3} {β : Type u_4} [inst : SemilatticeSup α] [inst_1 : Preorder β] {u : α → β},
Filter.Tendsto u Filter.atTop Filter.atTop → ∀ (a : α) (b : β), ∃ a' ≥ a, b ≤ u a'
This theorem, `Filter.exists_le_of_tendsto_atTop`, states that for any function `u` mapping elements from a type `α` with a 'semilattice sup' structure (a partially ordered set with a supremum operation) to a type `β` with a preorder structure, if the function `u` tends to infinity (represented by `Filter.atTop`) as its input tends to infinity, then for all elements `a` from `α` and `b` from `β`, there exists an element `a'` in `α` such that `a'` is greater than or equal to `a` and `b` is less than or equal to the value of the function `u` at `a'`. In other words, for any given `a` and `b`, we can always find a value `a'` such that `u(a')` is at least `b`, as the function `u` tends towards infinity.
More concisely: Given a semilattice `α` with supremum and a preordered type `β`, if a function `u : α → β` tends to `Filter.atTop β` as inputs tend to infinity, then for all `a ∈ α` and `b ∈ β`, there exists `a' ≥ a` such that `u a' ≤ b`.
|
Filter.eventually_le_atBot
theorem Filter.eventually_le_atBot : ∀ {α : Type u_3} [inst : Preorder α] (a : α), ∀ᶠ (x : α) in Filter.atBot, x ≤ a
This theorem states that for any type `α` that has an order (a `Preorder`), and for any element `a` of type `α`, at the limit of the sequence going to negative infinity (`atBot`), all elements `x` of the sequence will eventually be less than or equal to `a`. In mathematical terms, this means that for a sequence converging to negative infinity, there exists a point beyond which all elements of the sequence are less than or equal to a given value `a`.
More concisely: For any sequence converging to negative infinity in a preordered type, all elements beyond a certain point are less than or equal to any given element.
|
Filter.tendsto_atTop_add_right_of_le'
theorem Filter.tendsto_atTop_add_right_of_le' :
∀ {α : Type u_3} {β : Type u_4} [inst : OrderedAddCommGroup β] (l : Filter α) {f g : α → β} (C : β),
Filter.Tendsto f l Filter.atTop →
(∀ᶠ (x : α) in l, C ≤ g x) → Filter.Tendsto (fun x => f x + g x) l Filter.atTop
This theorem states that for any types `α` and `β` where `β` forms an ordered additive commutative group, given a filter `l` on `α` and two functions `f` and `g` from `α` to `β`, and a value `C` from `β`, if the function `f` tends to infinity under the filter `l`, and eventually for every `x` in `α`, `C` is less than or equal to `g(x)` under the filter `l`, then the function that maps `x` to the sum of `f(x)` and `g(x)` also tends to infinity under the filter `l`. In simpler terms, if `f` goes to infinity and `g` is eventually at least some constant `C`, then the sum of `f` and `g` also goes to infinity.
More concisely: If `f` tends to infinity and `C ≤ g(x)` for all `x` eventually under filter `l`, then the function `x ↦ f(x) + g(x)` tends to infinity under filter `l`.
|
Filter.atBot_Iio_eq
theorem Filter.atBot_Iio_eq :
∀ {α : Type u_3} [inst : SemilatticeInf α] (a : α), Filter.atBot = Filter.comap Subtype.val Filter.atBot
This theorem states that for any type `α` that forms a meet-semilattice (which is an algebraic structure with an operation that is associative, commutative, and idempotent, and also has an order relation consistent with this operation), and for any element `a` of that type, the `atBot` filter for an open interval `Iio a` (which represents the set of numbers less than `a`) is derived from the `atBot` filter in the overall order structure. In other words, the limit of the sequence approaching negative infinity within the interval is just a reflection of the limit of the sequence approaching negative infinity in the entire set, mapped by the `Subtype.val` function.
More concisely: For any meet-semilattice type `α` and element `a` of `α`, the `atBot` filter of the open interval `Iio a` is equal to the restriction of the `atBot` filter on `α` to the subtype `Subtype a α`.
|
Filter.unbounded_of_tendsto_atTop
theorem Filter.unbounded_of_tendsto_atTop :
∀ {α : Type u_3} {β : Type u_4} [inst : Nonempty α] [inst : SemilatticeSup α] [inst_1 : Preorder β]
[inst_2 : NoMaxOrder β] {f : α → β}, Filter.Tendsto f Filter.atTop Filter.atTop → ¬BddAbove (Set.range f)
This theorem states that for any function `f` from a type `α`, which is nonempty and has a semilattice structure with supremum, to another type `β`, which has a preorder structure and no maximum element, if `f` tends to infinity (represented by `Filter.atTop`) as its argument tends to infinity, then the range of `f` is not bounded above. In other words, if `f` grows without bound as its input grows without bound, there is no upper bound for the values of `f`.
More concisely: If `f` is a function from a nonempty, supremum-preserving `α` to a preordered `β` without a maximum element, and `f` grows without bound as `α` approaches infinity, then the range of `f` has no upper bound.
|
Filter.tendsto_const_mul_atTop_iff_pos
theorem Filter.tendsto_const_mul_atTop_iff_pos :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α}
[inst_1 : l.NeBot],
Filter.Tendsto f l Filter.atTop → (Filter.Tendsto (fun x => r * f x) l Filter.atTop ↔ 0 < r)
The theorem `Filter.tendsto_const_mul_atTop_iff_pos` states that for any types `α` and `β` with `α` being a Linear Ordered Semifield, given a nontrivial filter `l` of type `β`, a function `f` from `β` to `α`, and a constant `r` of type `α`, if the function `f` tends to infinity along the filter `l`, then the function that multiplies the output of `f` by `r` (i.e., `fun x => r * f x`) also tends to infinity along the same filter if and only if the constant `r` is greater than zero.
More concisely: If `α` is a Linear Ordered Semifield, `l` is a nontrivial filter on `β`, `f: β -> α`, `r > 0` in `α`, and `f` tends to infinity along `l`, then the function `x => r * f x` also tends to infinity along `l`.
|
Filter.map_val_Ioi_atTop
theorem Filter.map_val_Ioi_atTop :
∀ {α : Type u_3} [inst : SemilatticeSup α] [inst_1 : NoMaxOrder α] (a : α),
Filter.map Subtype.val Filter.atTop = Filter.atTop
This theorem states that for any type `α` that is a semilattice with supremum and has no maximum element, and for any value `a` of the type `α`, the image of the filter `atTop` on the set of all elements greater than `a` under the function `Subtype.val` (which extracts the underlying element from a subtype), is equal to the filter `atTop`. In other words, mapping the filter of all elements larger than a given value `a` in a semi-lattice via the extraction function results in the filter of all elements in the semilattice, assuming the semilattice has no maximum element.
More concisely: For any semilattice `α` without a maximum element and any `a` in `α`, the filter of elements greater than `a` maps to the entire filter `atTop` under the extraction function `Subtype.val`.
|
Filter.mem_atBot
theorem Filter.mem_atBot : ∀ {α : Type u_3} [inst : Preorder α] (a : α), {b | b ≤ a} ∈ Filter.atBot
The theorem `Filter.mem_atBot` states that for any type `α` with a preorder relationship, and any element `a` of `α`, the set of all elements `b` such that `b` is less than or equal to `a`, is an element of the filter `atBot`. In other words, this theorem indicates that every downward-closed set `{b | b ≤ a}` is included in the filter representing the limit towards negative infinity (`Filter.atBot`) on a preordered set.
More concisely: For any preordered type `α` and element `a` in `α`, the downward-closed set `{b | b ≤ a}` is a subset of the filter `Filter.atBot`.
|
Filter.high_scores
theorem Filter.high_scores :
∀ {β : Type u_4} [inst : LinearOrder β] [inst_1 : NoMaxOrder β] {u : ℕ → β},
Filter.Tendsto u Filter.atTop Filter.atTop → ∀ (N : ℕ), ∃ n ≥ N, ∀ k < n, u k < u n
This theorem, called `Filter.high_scores`, states that if `u` is a sequence of elements of some linearly ordered type `β`, with no maximum element, that tends to infinity, then for any given natural number `N`, there exists a natural number `n` greater than or equal to `N` such that all previous elements of the sequence `u` are strictly less than `u n`. In other words, if a sequence is unbounded above, then it continually reaches new high scores beyond any given point.
More concisely: Given a monotonically increasing, unbounded sequence `u` in a linearly ordered type, there exists `n` greater than any given natural number `N` such that `u n` is strictly greater than all preceding terms `u i` for `i < n`.
|
Function.Injective.map_atTop_finset_prod_eq
theorem Function.Injective.map_atTop_finset_prod_eq :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid α] {g : γ → β},
Function.Injective g →
∀ {f : β → α},
(∀ x ∉ Set.range g, f x = 1) →
Filter.map (fun s => s.prod fun i => f (g i)) Filter.atTop =
Filter.map (fun s => s.prod fun i => f i) Filter.atTop
The theorem states that given two functions `g : γ → β` and `f : β → α`, where `g` is injective and `f` maps to a commutative monoid `α`, if the value of the function `f` is `1` for all `x` outside the range of `g`, then the filters `atTop.map (fun s ↦ ∏ i in s, f (g i))` and `atTop.map (fun s ↦ ∏ i in s, f i)` are equal. In other words, if we consider sequences approaching infinity (`atTop`), the product of the sequence's `f(g(i))` values is the same as the product of the sequence's `f(i)` values when `f` is `1` outside the range of `g`.
This theorem is used in additive form to prove the equality `∑' x, f (g x) = ∑' y, f y` under the same conditions.
More concisely: Given injective function `g : γ → β` with image `β⊆α` and commutative monoid homomorphism `f : β → α` such that `f x = 1` for all `x ∉ Im(g),` the filters `atTop.map (fun s ↦ ∏ i in s, f (g i))` and `atTop.map (fun s ↦ ∏ i in s, f i)` are equal.
|
Filter.tendsto_atTop_atTop_of_monotone'
theorem Filter.tendsto_atTop_atTop_of_monotone' :
∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder ι] [inst_1 : LinearOrder α] {u : ι → α},
Monotone u → ¬BddAbove (Set.range u) → Filter.Tendsto u Filter.atTop Filter.atTop
The theorem states that for any function `u` from a type `ι` with a preorder to a type `α` with a linear order, if `u` is monotone and its range is not bounded above, then the function `u` tends to infinity as its input tends to infinity. In other words, if `u` is a monotone function and there is no upper limit to the values it can take, then as we increase the inputs to `u` without bound, the output of `u` will also increase without bound.
More concisely: If `u` is a monotone function from a preordered type `ι` to an ordered type `α` with no upper bound on its image, then for any `x in ι`, `u(x)` approaches infinity as `x` approaches the limit point of `ι`.
|
OrderIso.map_atBot
theorem OrderIso.map_atBot :
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β),
Filter.map (⇑e) Filter.atBot = Filter.atBot
This theorem states that for any two types `α` and `β` each equipped with a preorder relation, and given an order-preserving isomorphism `e` from `α` to `β`, the image under `e` of the filter `atBot` (representing the limit towards negative infinity) in `α` is equal to the filter `atBot` in `β`. In other words, `e` preserves the structure of "going to negative infinity" in the ordered sets. This is crucial for proving similar behavior of limits in different ordered spaces connected by such an isomorphism.
More concisely: Given order-preserving isomorphisms between preordered types, the image of the filter of bottom elements under the isomorphism is equal to the filter of bottom elements in the target type.
|
Filter.comap_embedding_atTop
theorem Filter.comap_embedding_atTop :
∀ {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : Preorder γ] {e : β → γ},
(∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) → (∀ (c : γ), ∃ b, c ≤ e b) → Filter.comap e Filter.atTop = Filter.atTop
The theorem `Filter.comap_embedding_atTop` states that for any two types `β` and `γ` with preorder relations, and any function `e` from `β` to `γ`, if `e` preserves the order (i.e., `e b₁` is less than or equal to `e b₂` if and only if `b₁` is less than or equal to `b₂`) and for every element `c` in `γ` there exists an element `b` in `β` such that `c` is less than or equal to `e b`, then the preimage filter (`Filter.comap e`) of the filter at infinity (`Filter.atTop`) on `γ` is the filter at infinity on `β`. In other words, under these conditions, the function `e` preserves the concept of "going to infinity".
More concisely: If `e: β -> γ` is a monotonic function such that for every `c in γ`, there exists `b in β` with `c <= e(b)`, then `Filter.comap e (Filter.atTop γ) = Filter.atTop β`.
|
Filter.map_atTop_finset_prod_le_of_prod_eq
theorem Filter.map_atTop_finset_prod_le_of_prod_eq :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid α] {f : β → α} {g : γ → α},
(∀ (u : Finset γ),
∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ (u'.prod fun x => g x) = v'.prod fun b => f b) →
Filter.map (fun s => s.prod fun b => f b) Filter.atTop ≤
Filter.map (fun s => s.prod fun x => g x) Filter.atTop
This theorem states that for any two functions `f` and `g` mapping to the same commutative monoid, if for every finite set `u` of elements in the domain of `g`, there is a finite set `v` such that for every super set `v'` of `v`, there exists a super set `u'` of `u` where the product of `g` over `u'` equals the product of `f` over `v'`, then the filter of the limit points of the product of `f` over infinite sets (`s → ∞`) is a subset of the filter of the limit points of the product of `g` over infinite sets. This provides a condition to compare the limit points of the infinite product of two functions.
More concisely: If functions `f` and `g` map to the same commutative monoid, and for every finite set `u` in the domain of `g`, there exists a finite set `v` such that the product of `g` over every super set of `v` equals the product of `f` over every super set of `u`, then the filter of limit points of `f` over infinite sets is a subset of the filter of limit points of `g` over infinite sets.
|
Filter.tendsto_mul_const_atTop_iff_pos
theorem Filter.tendsto_mul_const_atTop_iff_pos :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α}
[inst_1 : l.NeBot],
Filter.Tendsto f l Filter.atTop → (Filter.Tendsto (fun x => f x * r) l Filter.atTop ↔ 0 < r)
This theorem states that for any types `α` and `β`, with `α` being a linearly ordered semifield, a nontrivial filter `l` on `β`, a function `f` from `β` to `α`, and a constant `r` in `α`, if `f` tends to infinity along `l`, then the function `f` multiplied by `r` also tends to infinity if and only if `r` is positive. In other words, scaling a function that tends to infinity by a positive factor still results in a function that tends to infinity.
More concisely: For any linearly ordered semifield `α`, types `α` and `β`, nontrivial filter `l` on `β`, function `f` from `β` to `α`, and constant `r` in `α` with `r > 0`, if `f` tends to infinity along `l`, then `rf` also tends to infinity along `l`.
|
Filter.Tendsto.atTop_mul_neg_const
theorem Filter.Tendsto.atTop_mul_neg_const :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α},
r < 0 → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x * r) l Filter.atBot
This theorem states that if a function `f` tends to infinity along a given filter `l`, then the function `f` multiplied by a negative constant `r` on the right tends to negative infinity along the same filter `l`. In other words, if the values of `f` increase without bound when evaluated at points in the filter `l`, then the values of the product of `f` and a negative number `r` decrease without bound. This is applicable in the context of a linearly ordered field.
More concisely: If a function `f` approaches infinity along filter `l` in a linearly ordered field, then the function `rf` where `r` is a negative constant, approaches negative infinity along `l`.
|
Filter.tendsto_atBot_embedding
theorem Filter.tendsto_atBot_embedding :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {e : β → γ}
{l : Filter α},
(∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) →
(∀ (c : γ), ∃ b, e b ≤ c) → (Filter.Tendsto (e ∘ f) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot)
The theorem `Filter.tendsto_atBot_embedding` states that for any types `α`, `β`, and `γ`, given a preorder on `β` and `γ`, a function `f` from `α` to `β`, an order-preserving embedding `e` from `β` to `γ`, and a filter `l` on `α`, if for every value `c` in `γ`, there exists a value `b` in `β` such that `e(b)` is less than or equal to `c`, then the function `f` approaches negative infinity (i.e., `Filter.atBot`) under the filter `l` if and only if the composed function `e ∘ f` also approaches negative infinity under filter `l`.
In simpler words, this theorem asserts that a function's behavior of tending towards negative infinity is preserved under an order-preserving embedding.
More concisely: Given a function `f: α → β`, an order-preserving embedding `e: β → γ`, a preorder on `β` and `γ`, and a filter `l` on `α`, if for every `c` in `γ`, there exists `b` in `β` with `e(b) ≤ c`, then `f` tends to negative infinity under `l` if and only if `e ∘ f` tends to negative infinity under `l`.
|
Filter.tendsto_atTop_finset_of_monotone
theorem Filter.tendsto_atTop_finset_of_monotone :
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {f : β → Finset α},
Monotone f → (∀ (x : α), ∃ n, x ∈ f n) → Filter.Tendsto f Filter.atTop Filter.atTop
The theorem states that if we have a monotone sequence of finite sets (i.e., `Finset`s) represented by a function `f` from a type `β` with a preorder structure to `Finset α`, then, under the conditions that this function is monotone and that every element of type `α` belongs to at least one of the sets `f n`, the function `f` tends to infinity (or `atTop`) as `n` tends to infinity. This essentially means that for any given subset of `Finset α` that lies above a certain point, there exists a point in `β` beyond which all the `f n`'s are in that subset. In more concrete terms, the larger the input `n` to the function `f`, the larger the output set `f n`.
More concisely: Given a monotone function `f` from a preordered type `β` to `Finset α` such that every element of `α` belongs to some `f n`, then `f` tends to the set of all elements in `Finset α` as `n` tends to infinity.
|
Filter.frequently_high_scores
theorem Filter.frequently_high_scores :
∀ {β : Type u_4} [inst : LinearOrder β] [inst_1 : NoMaxOrder β] {u : ℕ → β},
Filter.Tendsto u Filter.atTop Filter.atTop → ∃ᶠ (n : ℕ) in Filter.atTop, ∀ k < n, u k < u n
The theorem `Filter.frequently_high_scores` states that for any sequence `u` of elements of a certain type `β`, which is a linear order without a maximum element, if `u` tends to infinity (`Filter.atTop`), then there are frequently (which means for infinitely many `n`) elements in this sequence such that the `n`-th element of `u` is strictly greater than all previous elements. That is, the sequence `u` often reaches new high scores.
More concisely: If `u` is a sequence in a linear order without a maximum element that tends to infinity, then there exist infinitely many indices `n` such that `u(n) > u(i)` for all `i < n`.
|
Filter.tendsto_mul_const_atTop_iff_neg
theorem Filter.tendsto_mul_const_atTop_iff_neg :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [inst_1 : l.NeBot],
Filter.Tendsto f l Filter.atBot → (Filter.Tendsto (fun x => f x * r) l Filter.atTop ↔ r < 0)
The theorem `Filter.tendsto_mul_const_atTop_iff_neg` states that for any types `α` and `β` where `α` is a linear ordered field, given a nontrivial filter `l` on `β`, a function `f` from `β` to `α`, and a constant `r` in `α`, if `f` tends to negative infinity along `l`, then the function which maps `x` to `f(x) * r` tends to positive infinity along `l` if and only if `r` is less than zero. This essentially says that multiplying a function that tends to negative infinity by a negative constant flips its direction and makes it tend to positive infinity.
More concisely: For a linear ordered field `α`, nontrivial filter `l` on `β`, function `f` from `β` to `α`, and constant `r` in `α`, `f` tends to negative infinity along `l` implies that `f * r` tends to positive infinity along `l` if and only if `r` is negative.
|
Filter.frequently_low_scores
theorem Filter.frequently_low_scores :
∀ {β : Type u_4} [inst : LinearOrder β] [inst_1 : NoMinOrder β] {u : ℕ → β},
Filter.Tendsto u Filter.atTop Filter.atBot → ∃ᶠ (n : ℕ) in Filter.atTop, ∀ k < n, u n < u k
The theorem `Filter.frequently_low_scores` states that, for any sequence `u` of data type `β` which is unbounded below (meaning that there is no minimum value `β` that the sequence can approach) and has a linear order, if the limit of the function `u` tends to minus infinity (`Filter.atBot`), then there are frequently (`∃ᶠ`) natural numbers `n` such that for all `k` smaller than `n`, the `n`th term of the sequence `u` is strictly smaller than the `k`th term. In other words, the sequence `u` often reaches a new low point.
More concisely: If `u` is an unbounded below, linearly ordered sequence of type `β` with limit approaching `-∞`, then there exist natural numbers `n` such that `u(n)` is strictly smaller than `u(k)` for all `k` < `n`.
|
Filter.eventually_atTop
theorem Filter.eventually_atTop :
∀ {α : Type u_3} [inst : SemilatticeSup α] [inst_1 : Nonempty α] {p : α → Prop},
(∀ᶠ (x : α) in Filter.atTop, p x) ↔ ∃ a, ∀ b ≥ a, p b
The theorem `Filter.eventually_atTop` states that for any type `α` which is a semilattice and is nonempty, and for any predicate `p` on `α`, the property `p` holds eventually as `x` approaches infinity (i.e., for all `x` beyond some point) if and only if there exists a value `a` in `α` such that `p` holds for all `b` greater than or equal to `a`. In other words, it provides an equivalence between "eventually for all `x` in the limit towards infinity, `p x` holds" and "there exists an `a` such that for all `b` that are greater than or equal to `a`, `p b` holds".
More concisely: For any semilattice type `α` and predicate `p` on `α`, ` Filter.eventually_atTop α p` holds if and only if there exists an element `a` in `α` such that for all `b` greater than or equal to `a`, `p b` holds.
|
Filter.tendsto_atTop_add_left_of_le'
theorem Filter.tendsto_atTop_add_left_of_le' :
∀ {α : Type u_3} {β : Type u_4} [inst : OrderedAddCommGroup β] (l : Filter α) {f g : α → β} (C : β),
(∀ᶠ (x : α) in l, C ≤ f x) →
Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x + g x) l Filter.atTop
The theorem `Filter.tendsto_atTop_add_left_of_le'` states that for all types `α` and `β`, where `β` is an ordered additive commutative group, given a filter `l` on `α` and two functions `f` and `g` from `α` to `β`, and a constant `C` from `β`. If for almost all `x` in `l`, `C` is less than or equal to `f(x)`, and if `g` tends to infinity as `x` tends to `l`, then the function `f(x) + g(x)` also tends to infinity as `x` tends to `l`. In other words, if `f(x)` is bounded below by a constant for almost all `x` in the filter and `g(x)` goes to infinity, then their sum also goes to infinity.
More concisely: If a filter converges to a point in an ordered additive commutative group, and the function values of another function, which is bounded below by a constant for almost all points in the filter and tends to infinity, are added to the function values of a third function in the filter, then the sum also tends to infinity.
|
Filter.Tendsto.neg_const_mul_atBot
theorem Filter.Tendsto.neg_const_mul_atBot :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α},
r < 0 → Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => r * f x) l Filter.atTop
The theorem `Filter.Tendsto.neg_const_mul_atBot` states that for any types `α` and `β`, where `α` is a linearly ordered field, any filter `l` over `β`, any function `f` from `β` to `α`, and any real number `r` in `α` that is less than zero, if the function `f` tends to negative infinity along the filter `l`, then the function that multiplies `f` by `r` (corresponding to multiplying `f` on the left by a negative constant) tends to positive infinity along the same filter `l`.
More concisely: If `f: β → α` tends to negative infinity along filter `l` over `β` in the linearly ordered field `α`, then the function `(-r) * f` tends to positive infinity along `l`, for any `r < 0` in `α`.
|
Filter.eventually_atBot
theorem Filter.eventually_atBot :
∀ {α : Type u_3} [inst : SemilatticeInf α] [inst_1 : Nonempty α] {p : α → Prop},
(∀ᶠ (x : α) in Filter.atBot, p x) ↔ ∃ a, ∀ b ≤ a, p b
This theorem states that for any type `α` that is a semilattice with respect to the infimum operation and is nonempty, and for any proposition `p` that applies to elements of `α`, the proposition `p` holds eventually at negative infinity (as represented by `Filter.atBot`) if and only if there exists an element `a` in `α` such that `p` holds for all elements `b` that are less than or equal to `a`. In simpler terms, the proposition `p` is true for all sufficiently small values in the semilattice.
More concisely: For any semilattice `α` with nonempty infimum `⊥` and proposition `p` over `α`, `Filter.atBot p` holds if and only if there exists an element `a` such that `p` holds for all `b ≤ a`.
|
Filter.tendsto_const_mul_atBot_iff
theorem Filter.tendsto_const_mul_atBot_iff :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [inst_1 : l.NeBot],
Filter.Tendsto (fun x => r * f x) l Filter.atBot ↔
0 < r ∧ Filter.Tendsto f l Filter.atBot ∨ r < 0 ∧ Filter.Tendsto f l Filter.atTop
The theorem `Filter.tendsto_const_mul_atBot_iff` states that for a function `f` mapping from an arbitrary type `β` to a linear ordered field `α`, and a constant `r` in `α`, the function `fun x ↦ r * f x` tends to negative infinity along a nontrivial filter `l` if and only if either `r > 0` and the original function `f` tends to negative infinity along `l`, or `r < 0` and `f` tends to positive infinity along `l`. Essentially, this theorem is capturing the intuition that multiplying a function by a positive constant preserves the direction of its limit, while multiplying by a negative constant reverses it.
More concisely: For a function `f` from type `β` to a linear ordered field `α` and a constant `r` in `α`, the function `x ↦ r * f x` tends to negative infinity along a nontrivial filter `l` if and only if `r < 0` and `f` tends to positive infinity along `l`, or `r > 0` and `f` tends to negative infinity along `l`.
|
Filter.eventually_ge_atTop
theorem Filter.eventually_ge_atTop : ∀ {α : Type u_3} [inst : Preorder α] (a : α), ∀ᶠ (x : α) in Filter.atTop, a ≤ x
The theorem `Filter.eventually_ge_atTop` asserts that for any type `α` that is equipped with a preorder, and for any element `a` from that type, all points `x` in the filter `atTop` (which represents the limit to infinity) will eventually (or at some point) satisfy the condition that `a` is less than or equal to `x`. In simple terms, beyond a certain point in the order, all elements are greater than or equal to `a`.
More concisely: For any preordered type `α` and element `a` in `α`, all elements `x` in the filter of upper bounds `atTop` eventually satisfy `a ≤ x`.
|
Filter.frequently_atTop
theorem Filter.frequently_atTop :
∀ {α : Type u_3} [inst : SemilatticeSup α] [inst_1 : Nonempty α] {p : α → Prop},
(∃ᶠ (x : α) in Filter.atTop, p x) ↔ ∀ (a : α), ∃ b ≥ a, p b
The theorem `Filter.frequently_atTop` states that for any type `α` that forms a semilattice under a supremum operation and is nonempty, and for any property `p` from `α` to `Prop`, the property `p` holds "frequently" at the limit towards infinity (`Filter.atTop`) if and only if, for every element `a` of `α`, there exists an element `b` greater than or equal to `a` such that `p` holds for `b`. To put it simply, the property is satisfied somewhere beyond every point in the ordered set.
More concisely: For any semilattice with supremum `α` and nonempty `p : α -> Prop`, `Filter.atTop p` holds if and only if for all `a : α`, there exists `b : α` with `b >= a` such that `p b` holds.
|
Filter.tendsto_atTop_mono
theorem Filter.tendsto_atTop_mono :
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {l : Filter α} {f g : α → β},
(∀ (n : α), f n ≤ g n) → Filter.Tendsto f l Filter.atTop → Filter.Tendsto g l Filter.atTop
The theorem `Filter.tendsto_atTop_mono` states that for any types `α` and `β` where `β` is a preordered set, along with a filter `l` on `α` and two functions `f` and `g` from `α` to `β`, if for every element `n` from `α`, `f(n)` is less than or equal to `g(n)`, then if the function `f` tends to infinity (`Filter.atTop`) with respect to the filter `l`, the function `g` also tends to infinity with respect to the same filter `l`. In other words, if `f` is pointwise less than or equal to `g` and `f` tends towards infinity, then `g` must also tend towards infinity.
More concisely: If `f` is pointwise less than or equal to `g` and `f` tends to infinity with respect to filter `l`, then `g` also tends to infinity with respect to the same filter `l`.
|
Filter.Tendsto.eventually_ge_atTop
theorem Filter.Tendsto.eventually_ge_atTop :
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {f : α → β} {l : Filter α},
Filter.Tendsto f l Filter.atTop → ∀ (c : β), ∀ᶠ (x : α) in l, c ≤ f x
The theorem `Filter.Tendsto.eventually_ge_atTop` states that for any types `α` and `β`, where `β` has a preorder relation, and for any function `f` mapping from `α` to `β`, and for any filter `l` on `α`: if `f` tends to infinity (`Filter.atTop`) under the filter `l`, then for any value `c` in `β`, eventually (`∀ᶠ`) for every `x` in the domain `α` under the filter `l`, the value `c` is less than or equal to the value `f(x)`. In other words, if the function `f` tends to infinity at the filter `l`, then there exists a point after which all values of the function `f` are greater than or equal to any given value `c`.
More concisely: If a function from type `α` to preordered type `β` tends to infinity under filter `l` on `α`, then for any `c` in `β`, there exists an element `x` in the filter `l` such that `f(x) ≥ c`.
|
Filter.Ici_mem_atTop
theorem Filter.Ici_mem_atTop : ∀ {α : Type u_3} [inst : Preorder α] (a : α), Set.Ici a ∈ Filter.atTop
The theorem `Filter.Ici_mem_atTop` states that for any type `α` equipped with a preorder, and for any element `a` of that type, the set of all elements greater than or equal to `a` (`Set.Ici a`) is a member of the filter representing the limit towards positive infinity (`Filter.atTop`). In other words, as we go towards positive infinity in our ordered set, we will always encounter the set of elements that are greater than or equal to a given element `a`.
More concisely: For any preordered type `α` and element `a` in `α`, the upward-closed set `{x : α | x ≥ a}` is a member of the filter `Filter.atTop`.
|
Function.Injective.map_atTop_finset_sum_eq
theorem Function.Injective.map_atTop_finset_sum_eq :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid α] {g : γ → β},
Function.Injective g →
∀ {f : β → α},
(∀ x ∉ Set.range g, f x = 0) →
Filter.map (fun s => s.sum fun i => f (g i)) Filter.atTop =
Filter.map (fun s => s.sum fun i => f i) Filter.atTop
The theorem `Function.Injective.map_atTop_finset_sum_eq` states the following:
Consider two functions, `g : γ → β` which is injective, and `f : β → α` where `α` is an additive commutative monoid. Suppose that for any `x` not in the range of `g`, `f(x)` is zero. Under these conditions, the theorem asserts the equality of two filters. The first filter is defined by mapping `atTop` using the function which, given a set, returns the sum of `f(g(i))` for each element `i` in the set. The second filter is likewise defined by mapping `atTop` using a function which, given a set, sums up `f(i)` for each element `i` in the set. This statement is used in the proof of the equality `∑' x, f (g x) = ∑' y, f y` under the same conditions.
More concisely: Given an injective function `g : γ → β` such that `f : β → α` maps outside the range of `g` to zero, the filters obtained by mapping `atTop` using `f ∘ g` and `f` are equal.
|
Filter.tendsto_const_mul_atBot_of_neg
theorem Filter.tendsto_const_mul_atBot_of_neg :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α},
r < 0 → (Filter.Tendsto (fun x => r * f x) l Filter.atBot ↔ Filter.Tendsto f l Filter.atTop)
The theorem `Filter.tendsto_const_mul_atBot_of_neg` states that, given a negative constant `r`, a function `f` that takes an input of type `β` and returns an output of type `α` (where `α` is a linearly ordered field), and a filter `l` on `β`, the function `f` tends to positive infinity with respect to the filter `l` if and only if the function given by `x ↦ r * f(x)` tends to negative infinity with respect to the same filter `l`. In other words, if `f` grows without bound along `l`, then `r * f` descends without bound along `l`, provided `r` is a negative constant.
More concisely: For a negative constant `r` and a function `f` from a linearly ordered field `β` to a linearly ordered field `α`, if `f` tends to positive infinity with respect to filter `l` on `β`, then `r * f` tends to negative infinity with respect to the same filter `l`.
|
Filter.Tendsto.atTop_mul_atTop
theorem Filter.Tendsto.atTop_mul_atTop :
∀ {α : Type u_3} {β : Type u_4} [inst : OrderedSemiring α] {l : Filter β} {f g : β → α},
Filter.Tendsto f l Filter.atTop →
Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x * g x) l Filter.atTop
The theorem `Filter.Tendsto.atTop_mul_atTop` states that for any ordered semiring `α`, any type `β`, any filter `l` of type `β`, and any two functions `f` and `g` from `β` to `α`, if `f` and `g` both tend towards infinity (represented by `Filter.atTop`) as the values from filter `l` go towards infinity, then the function that maps each value from filter `l` to the product of `f` and `g` at that value also tends towards infinity. In other words, the limit of the product of two functions, each tending to infinity, is also infinity.
More concisely: If two functions from a filter over a type to an ordered semiring both tend towards infinity, then their product also tends towards infinity with respect to that filter.
|
Mathlib.Order.Filter.AtTopBot._auxLemma.23
theorem Mathlib.Order.Filter.AtTopBot._auxLemma.23 :
∀ {α : Type u_3} {β : Type u_4} [inst : OrderedAddCommGroup β] {l : Filter α} {f : α → β},
Filter.Tendsto f l Filter.atBot = Filter.Tendsto (fun x => -f x) l Filter.atTop
The theorem `Mathlib.Order.Filter.AtTopBot._auxLemma.23` states that for any types `α` and `β`, where `β` is an ordered additive commutative group, and given a filter `l` on type `α` and a function `f` from `α` to `β`, the function `f` tends towards negative infinity (`Filter.atBot`) along the filter `l` if and only if the function that sends `x` to `-f(x)` tends towards positive infinity (`Filter.atTop`) along the same filter `l`. In other words, reversing the direction of a function flips the direction it tends to infinity.
More concisely: For any filter `l` on type `α`, function `f` from `α` to an ordered additive commutative group `β`, the function `f` tends towards negative infinity along `l` if and only if the function `-f` tends towards positive infinity along `l`.
|
Filter.Tendsto.const_mul_atBot
theorem Filter.Tendsto.const_mul_atBot :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α},
0 < r → Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => r * f x) l Filter.atBot
The theorem `Filter.Tendsto.const_mul_atBot` states that if a function `f`, which maps from an arbitrary type `β` to a type `α` defined over a linearly ordered field, tends to negative infinity along a given filter `l`, then if we multiply `f` by a positive constant `r`, this new function will also tend towards negative infinity along the same filter `l`. In other words, multiplying a function that tends to negative infinity by a positive constant does not change the limit behavior of the function.
More concisely: If a function `f : β → α` over a linearly ordered field tends to negative infinity along filter `l`, then the function `rf : β → α` defined by `rf x := r * f x` also tends to negative infinity along `l`, for any positive constant `r : ℝ`.
|
Filter.Tendsto.atBot_mul_neg_const
theorem Filter.Tendsto.atBot_mul_neg_const :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α},
r < 0 → Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => f x * r) l Filter.atTop
This theorem states that for any function `f` from type `β` to a linearly ordered field `α`, and any filter `l` on `β`, if `f` tends to negative infinity (meaning that the values of `f` become arbitrarily small) along `l`, and `r` is a negative constant in `α`, then the function obtained by multiplying `f` by `r` tends to positive infinity along `l`. In other words, multiplying a function that trends towards negative infinity by a negative constant results in a function that trends towards positive infinity.
More concisely: If `f` is a function from a linearly ordered type `β` to a linearly ordered field `α`, `l` is a filter on `β`, and `f` tends to negative infinity along `l`, then the function `rf` obtained by multiplying `f` with a negative constant `r` in `α` tends to positive infinity along `l`.
|
Filter.map_val_Ici_atTop
theorem Filter.map_val_Ici_atTop :
∀ {α : Type u_3} [inst : SemilatticeSup α] (a : α), Filter.map Subtype.val Filter.atTop = Filter.atTop
This theorem states that for any type `α` that is a semilattice (an ordered set in which every pair of elements has a least upper bound), and any element `a` of `α`, the image of the filter `atTop` (which represents the limit tending to infinity in the ordered set) on the interval `Ici a` (the set of all elements greater than or equal to `a`) under the coercion function `Subtype.val` (which extracts the underlying element from a subtype) is equal to `atTop`. In other words, the filter of all elements above a certain point in a semilattice, when we consider just the underlying elements without the property that makes them a subtype, is still the filter of all elements above that point.
More concisely: For any semilattice `α` and element `a` in `α`, the image of the filter `atTop` on `Ici a` under `Subtype.val` equals `atTop`. Alternatively, the filter of all elements above `a` in a semilattice, when considered as underlying elements, is still the filter of all elements above `a`.
|
Filter.exists_seq_tendsto
theorem Filter.exists_seq_tendsto :
∀ {α : Type u_3} (f : Filter α) [inst : f.IsCountablyGenerated] [inst : f.NeBot],
∃ x, Filter.Tendsto x Filter.atTop f
The theorem `Filter.exists_seq_tendsto` states that for any nontrivial countably generated filter `f` on a type `α`, there exists a sequence `x` that converges to `f`. In other words, for every neighborhood of `f`, all but finitely many elements of the sequence `x` are in that neighborhood. This is the notion of the sequence `x` tending to the filter `f` as it goes to infinity.
More concisely: For every nontrivial countably generated filter `f` on type `α`, there exists a sequence `x : α^ℕ` such that for every neighborhood `n` of `f`, all but finitely many elements of `x` belong to `n`.
|
Filter.tendsto_mul_const_atBot_iff
theorem Filter.tendsto_mul_const_atBot_iff :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [inst_1 : l.NeBot],
Filter.Tendsto (fun x => f x * r) l Filter.atBot ↔
0 < r ∧ Filter.Tendsto f l Filter.atBot ∨ r < 0 ∧ Filter.Tendsto f l Filter.atTop
The theorem `Filter.tendsto_mul_const_atBot_iff` states that for any type `α` in a linearly ordered field, any type `β`, a non-trivial filter `l` on `β`, a function `f` from `β` to `α`, and a real number `r`, the function `f(x) * r` tends to negative infinity along the filter `l` if and only if either `r` is positive and `f` tends to negative infinity along `l`, or `r` is negative and `f` tends to positive infinity along `l`. Hence, the sign of `r` decides whether `f` should tend to positive or negative infinity for `f(x) * r` to tend to negative infinity.
More concisely: For a function `f` from a linearly ordered field `β` to a real-valued type `α`, and a non-trivial filter `l` on `β`, the product `f(x) * r` tends to negative infinity along `l` if and only if either `r` is positive and `f` tends to negative infinity along `l`, or `r` is negative and `f` tends to positive infinity along `l`.
|
Filter.tendsto_abs_atBot_atTop
theorem Filter.tendsto_abs_atBot_atTop :
∀ {α : Type u_3} [inst : LinearOrderedAddCommGroup α], Filter.Tendsto abs Filter.atBot Filter.atTop
The theorem `Filter.tendsto_abs_atBot_atTop` states that for any type `α` that forms a linearly ordered additive commutative group, the limit of the absolute value function `abs` as `x` approaches negative infinity (`Filter.atBot`) is positive infinity (`Filter.atTop`). In other words, the absolute value of `x` increases without bound as `x` becomes increasingly negative. The notation used in the comment, $\lim_{x\to-\infty}|x|=+\infty$, is a standard mathematical way to express the same statement.
More concisely: For any linearly ordered additive commutative group type `α`, the absolute value function `abs` is unbounded below as `x` approaches negative infinity (`Filter.atBot`), i.e., `∀∞ x: α, abs x > 0`.
|
Filter.tendsto_atTop_atBot
theorem Filter.tendsto_atTop_atBot :
∀ {α : Type u_3} {β : Type u_4} [inst : Nonempty α] [inst : SemilatticeSup α] [inst_1 : Preorder β] {f : α → β},
Filter.Tendsto f Filter.atTop Filter.atBot ↔ ∀ (b : β), ∃ i, ∀ (a : α), i ≤ a → f a ≤ b
The theorem `Filter.tendsto_atTop_atBot` states that for any function `f` from a nonempty type `α` equipped with a semilattice and preorder structure to a type `β` with a preorder structure, `f` tends to negative infinity (represented by `Filter.atBot`) as `α` tends to positive infinity (represented by `Filter.atTop`) if and only if for every element `b` of `β`, there exists an element `i` in `α` such that for all elements `a` of `α` greater than or equal to `i`, the value of `f` at `a` is less than or equal to `b`. This essentially captures the idea that as we go to higher and higher elements in `α`, the function `f` goes to lower and lower elements in `β`.
More concisely: For a function between two semilattices with preorders, it tends to negative infinity as the domain tends to positive infinity if and only if for every element in the target, there exists a domain element such that the function value is less than or equal to that target element for all greater domain elements.
|
Filter.tendsto_atBot
theorem Filter.tendsto_atBot :
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {m : α → β} {f : Filter α},
Filter.Tendsto m f Filter.atBot ↔ ∀ (b : β), ∀ᶠ (a : α) in f, m a ≤ b
The theorem `Filter.tendsto_atBot` states that for any type `α`, type `β` with a preorder structure, a function `m` mapping from `α` to `β`, and a filter `f` on `α`, the function `m` tends to `-∞` along `f` if and only if for every `b` of type `β`, it is eventually true in `f` that `(m a) ≤ b` for all `a` of type `α`. In other words, the function `m` approaches negative infinity at the rate defined by the filter `f` if and only if for any value `b` in `β`, there exists a point in `f` after which all function values `m a` are less than or equal to `b`.
More concisely: For any preorder type `β`, function `m` from type `α` to `β`, and filter `f` on `α`, `m` tends to negative infinity along `f` if and only if for every `b` in `β`, there exists an element `a` in `f` such that `m a` ≤ `b`.
|
Monotone.tendsto_atTop_finset
theorem Monotone.tendsto_atTop_finset :
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {f : β → Finset α},
Monotone f → (∀ (x : α), ∃ n, x ∈ f n) → Filter.Tendsto f Filter.atTop Filter.atTop
The theorem `Monotone.tendsto_atTop_finset` states that, for any types `α` and `β` and a preorder on `β`, if `f` is a monotone function from `β` to sets of `α` (`Finset α`), and every element `x` of type `α` is in the set `f n` for some `n` of type `β`, then `f` tends to `atTop` as `n` tends to `atTop`. In other words, if `f` is a monotone sequence of finite sets `Finset α` that includes every `α` in some set `f n`, then `f` approaches the limit of `atTop` as `n` approaches `atTop`. This implies that the sequence `f` grows to cover all of `α` as `n` grows.
More concisely: If `f` is a monotonic function from a preordered type `β` to sets of type `α`, and every `α` element is in some `f(n)` for some `n` approaching the top element `atTop` of `β`, then `f` tends to the limit `atTop` as `n` tends to `atTop`.
|
Filter.Tendsto.const_mul_atTop
theorem Filter.Tendsto.const_mul_atTop :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α},
0 < r → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => r * f x) l Filter.atTop
The theorem `Filter.Tendsto.const_mul_atTop` states that for any types `α` and `β`, given a linearly ordered semifield `α`, a filter `l` on `β`, a function `f : β → α`, and a positive constant `r : α`, if the function `f` tends to infinity (i.e., increases without bound) along the filter `l`, then the function formed by multiplying `f` by `r` (i.e., `(fun x => r * f x)`) also tends to infinity along the same filter. For similar behavior in the specific cases of `ℕ` or `ℤ`, one should use `filter.tendsto.const_mul_atTop'`.
More concisely: If a function tends to infinity along a filter in a linearly ordered semifield, then multiplying it by a positive constant also tends to infinity along the same filter.
|
Filter.Ioi_mem_atTop
theorem Filter.Ioi_mem_atTop :
∀ {α : Type u_3} [inst : Preorder α] [inst_1 : NoMaxOrder α] (x : α), Set.Ioi x ∈ Filter.atTop
The theorem `Filter.Ioi_mem_atTop` states that for any type `α` with a `Preorder` relation (i.e., a binary relation that is reflexive and transitive) and without a maximum element (`NoMaxOrder`), for any element `x` of that type, the set of all elements greater than `x` (`Set.Ioi x`) is a member of the filter `atTop`. In other words, the set of all elements greater than `x` is a set that gets arbitrarily large (goes to infinity). This is captured by the filter `atTop`, which represents the limit tending to infinity in the ordered set `α`.
More concisely: For any type `α` with a `NoMaxOrder` `Preorder` relation, the set of elements strictly greater than any `x` in `α` belongs to the filter `atTop`.
|
Filter.map_val_Iic_atBot
theorem Filter.map_val_Iic_atBot :
∀ {α : Type u_3} [inst : SemilatticeInf α] (a : α), Filter.map Subtype.val Filter.atBot = Filter.atBot
The theorem `Filter.map_val_Iic_atBot` states that for any type `α` that forms a semilattice under an infimum operation, and for any element `a : α`, the `atBot` filter (representing a limit tending towards negative infinity) when applied to the subtype's underlying element (`Subtype.val`) is the same as the `atBot` filter in the ambient order. In other words, mapping a filter towards negative infinity in a subtype does not change the filter's behavior—it behaves the same way in the larger type as it would in the subtype.
More concisely: For any semilattice `α` with infimum operation and any subtype `s : Set α`, `Filter.map atBot (Subtype.val s) = atBot`, where `Filter.map` applies a filter to the image of a function and `atBot` is the filter representing a limit tending towards negative infinity.
|
Filter.atTop_Ici_eq
theorem Filter.atTop_Ici_eq :
∀ {α : Type u_3} [inst : SemilatticeSup α] (a : α), Filter.atTop = Filter.comap Subtype.val Filter.atTop
The theorem `Filter.atTop_Ici_eq` states that for any type `α` that has a semilattice structure, and any element `a : α`, the `atTop` filter for the open interval `Ici a` (which is the set of all elements that are greater than or equal to `a`) is the same as the `atTop` filter of the whole `α` type but viewed through the mapping 'Subtype.val'. Here, `Subtype.val` is a function that takes an element from a subtype and returns its underlying element in the base type. This theorem essentially says that the "going to infinity" behavior in the subset `Ici a` mirrors the "going to infinity" behavior in the whole set, when we relate elements of the subset to elements of the whole set via the natural inclusion mapping given by `Subtype.val`.
More concisely: For any semilattice type `α` and element `a : α`, the `atTop` filter of the open interval `Ici a` equals the `atTop` filter of `α` restricted to the elements greater than or equal to `a`.
|
Monotone.tendsto_atTop_atTop_iff
theorem Monotone.tendsto_atTop_atTop_iff :
∀ {α : Type u_3} {β : Type u_4} [inst : Nonempty α] [inst : SemilatticeSup α] [inst_1 : Preorder β] {f : α → β},
Monotone f → (Filter.Tendsto f Filter.atTop Filter.atTop ↔ ∀ (b : β), ∃ a, b ≤ f a)
This theorem states that for any two types `α` and `β`, where `α` is nonempty and a semilattice with supremum and `β` is a preorder, and a monotone function `f` from `α` to `β`, the function `f` tends to infinity as `α` tends to infinity if and only if for any `b` in `β`, there exists an `a` in `α` such that `b` is less than or equal to `f(a)`. This captures the intuition that a function that grows without bound as its argument does will always reach any prescribed value.
More concisely: For any nonempty semilattice `α` with supremum, preorder `β`, and monotone function `f` from `α` to `β`, `f` tends to infinity if and only if for every `b` in `β`, there exists an `a` in `α` such that `f(a) ≥ b`.
|
Filter.tendsto_mul_const_atTop_of_pos
theorem Filter.tendsto_mul_const_atTop_of_pos :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α},
0 < r → (Filter.Tendsto (fun x => f x * r) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop)
This theorem states that, given a positive constant `r`, a function `f` multiplied by `r` tends to infinity along a filter if and only if the function `f` itself tends to infinity along the same filter. In more mathematical terms, for any types `α` and `β`, a linear ordered semifield `α`, a filter `l` on `β`, a function `f` from `β` to `α`, and a positive constant `r` in `α`, `f(x) * r` tends to infinity as `x` approaches the limit defined by the filter `l` if and only if `f(x)` itself tends to infinity as `x` approaches the same limit.
More concisely: For any filter `l` on a type `β`, a function `f` from `β` to a linear ordered semifield `α`, and a positive constant `r` in `α`, `f` tends to infinity along `l` if and only if `f * r` does.
|
Filter.atBot_basis
theorem Filter.atBot_basis :
∀ {α : Type u_3} [inst : Nonempty α] [inst : SemilatticeInf α], Filter.atBot.HasBasis (fun x => True) Set.Iic := by
sorry
This theorem states that for any type `α` that is nonempty and has the structure of a semilattice with an infimum operation, the filter `Filter.atBot`, which represents the limit towards negative infinity in the order of `α`, has a basis. The basis is described by the constant function returning `True` and the left-infinite right-closed interval `Set.Iic`. In other words, every set in the `Filter.atBot` can be represented as a union of sets of the form `Set.Iic a` for some `a` in `α`, and every such set `Set.Iic a` is indeed in `Filter.atBot`.
More concisely: For any nonempty semilattice type `α` with an infimum operation, the filter `Filter.atBot` has a basis consisting of the constant function returning `True` and the left-infinite right-closed intervals `Set.Iic a` for all `a` in `α`.
|
Filter.tendsto_atTop
theorem Filter.tendsto_atTop :
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {m : α → β} {f : Filter α},
Filter.Tendsto m f Filter.atTop ↔ ∀ (b : β), ∀ᶠ (a : α) in f, b ≤ m a
This theorem states that for any types `α` and `β`, where `β` is an ordered set, and for any function `m` from `α` to `β` and any filter `f` on `α`, the function `m` tends to infinity along `f` (i.e., `Filter.Tendsto m f Filter.atTop`) if and only if, for any element `b` in `β`, eventually (for all elements `a` in the filter `f`) the value of `b` is less than or equal to `m a`. In mathematical terms, this can be written as:
\\[\forall b \in \beta, \, \exists a \in \alpha \, \text{in the filter} \, f \, \text{such that} \, b \leq m(a).\\]
The symbol "∀ᶠ" refers to the "eventually" quantifier, used in the context of filters: a statement is said to hold "eventually" if it holds in the filter outside of a finite subset.
More concisely: For any function from a type to an ordered set and any filter on the domain, the function tends to infinity along the filter if and only if every element in the range is eventually less than or equal to the function value for some element in the filter.
|
Filter.Tendsto.atBot_div_const
theorem Filter.Tendsto.atBot_div_const :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α},
0 < r → Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => f x / r) l Filter.atBot
The theorem `Filter.Tendsto.atBot_div_const` states that if a function `f`, that maps from an arbitrary type `β` to a linearly ordered field `α`, tends to negative infinity along a certain filter `l`, then the function `f` divided by a positive constant `r` from type `α` also tends to negative infinity along the same filter. The precondition is that `r` should be positive (`0 < r`) and the function `f` tends towards negative infinity (`Filter.Tendsto f l Filter.atBot`).
More concisely: If a function `f : β -> α` tends to negative infinity along filter `l` in a linearly ordered field `α`, then `(f : β -> α) / r` also tends to negative infinity along `l` for any positive constant `r : α`.
|
Filter.eventually_lt_atBot
theorem Filter.eventually_lt_atBot :
∀ {α : Type u_3} [inst : Preorder α] [inst_1 : NoMinOrder α] (a : α), ∀ᶠ (x : α) in Filter.atBot, x < a
This theorem, `Filter.eventually_lt_atBot`, states that for any given type `α` which has a `Preorder` and `NoMinOrder` structure, and for any element `a` of that type, eventually (for all sufficiently small `x`), `x` will be less than `a` as `x` approaches negative infinity (`Filter.atBot`). In other words, as `x` gets arbitrarily close to negative infinity, all such `x` will be less than `a`. This holds true for all preordered types that do not have a minimum element.
More concisely: For any type `α` with a `Preorder` and `NoMinOrder` structure, and any `a` in `α`, there exists a neighborhood of `Filter.atBot` such that `x < a` for all `x` in that neighborhood.
|
Filter.tendsto_const_mul_atTop_of_pos
theorem Filter.tendsto_const_mul_atTop_of_pos :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α},
0 < r → (Filter.Tendsto (fun x => r * f x) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop)
The theorem `Filter.tendsto_const_mul_atTop_of_pos` states that given a positive constant `r`, the function `f` multiplied by `r` tends to infinity along a particular filter if and only if the function `f` itself tends to infinity along the same filter. This holds for any filter `l` and any function `f` mapping from a type `β` to a type `α`, where `α` is a linear ordered semifield. In other words, scaling a function by a positive factor does not change the fact whether or not it tends to infinity.
More concisely: Given a positive constant `r` and a function `f` from a type `β` to a linear ordered semifield `α`, if `f` tends to infinity along a filter `l`, then `rf` also tends to infinity along `l`.
|
Filter.tendsto_atBot_atBot_of_monotone'
theorem Filter.tendsto_atBot_atBot_of_monotone' :
∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder ι] [inst_1 : LinearOrder α] {u : ι → α},
Monotone u → ¬BddBelow (Set.range u) → Filter.Tendsto u Filter.atBot Filter.atBot
The theorem `Filter.tendsto_atBot_atBot_of_monotone'` states that if `u` is a monotone function, with `ι` as its domain and `α` as its codomain where `α` is linearly ordered, and if the range of `u` is not bounded below, then `u` tends to negative infinity as its argument tends to negative infinity. In mathematical terms, if a function's output values are not bounded below and the function is monotone, then as the input values approach negative infinity, the output values will also approach negative infinity.
More concisely: If `u : ι -> α` is a monotone function with unbounded below domain `ι` and codomain `α` ordered by a linear order, then `u` tends to negative infinity as `x` approaches negative infinity in `ι`.
|
Monotone.tendsto_atTop_atTop
theorem Monotone.tendsto_atTop_atTop :
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Monotone f → (∀ (b : β), ∃ a, b ≤ f a) → Filter.Tendsto f Filter.atTop Filter.atTop
The theorem `Monotone.tendsto_atTop_atTop` states that, for all types `α` and `β` equipped with a preorder, if a function `f` from `α` to `β` is monotone, and for all `b` in `β` there exists an `a` in `α` such that `b` is less than or equal to `f(a)`, then the function `f` tends to infinity as its argument tends to infinity. In other words, as we take larger and larger values in the domain of `f`, the function values also become larger and larger. This is a property of monotone functions that do not have an upper bound.
More concisely: If `f` is a monotone function from type `α` to type `β`, where `α` and `β` have a preorder, and for each `b` in `β`, there exists an `a` in `α` with `f(a) ≤ b`, then `f` is unbounded.
|
Filter.tendsto_atTop_atTop_of_monotone
theorem Filter.tendsto_atTop_atTop_of_monotone :
∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Monotone f → (∀ (b : β), ∃ a, b ≤ f a) → Filter.Tendsto f Filter.atTop Filter.atTop
This theorem, `Filter.tendsto_atTop_atTop_of_monotone`, states that for all types `α` and `β` with preorders, if a function `f` from `α` to `β` is monotone (that is, for every pair of elements in `α` where the first is less than or equal to the second, the function value of the first element is less than or equal to the function value of the second) and for every element in `β`, there exists an element in `α` such that the function value of the `α` element is greater than or equal to the `β` element, then the function `f` tends to infinity with respect to the filter on `α` that represents the limit going to infinity (this is given by `Filter.atTop`), and similarly, the output of the function `f` also tends to infinity with respect to the filter on `β` that represents the limit going to infinity (also given by `Filter.atTop`). In other words, as the input of the function `f` approaches infinity, the output of the function `f` also approaches infinity.
More concisely: If `f` is a monotone function from `α` to `β` such that for every `y` in `β`, there exists `x` in `α` with `f x ≥ y`, then `f` is tendstoAtTop (`Filter.atTop`) on `α` and its image is tendstoAtTop on `β`.
|
Filter.tendsto_const_mul_atTop_of_neg
theorem Filter.tendsto_const_mul_atTop_of_neg :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α},
r < 0 → (Filter.Tendsto (fun x => r * f x) l Filter.atTop ↔ Filter.Tendsto f l Filter.atBot)
This theorem states that for any types `α` and `β`, given a linearly ordered field over `α`, a filter `l` over `β`, a function `f` mapping from `β` to `α`, and a negative constant `r` of type `α`, the function defined by multiplying `f(x)` by `r` tends to infinity along the filter `l` if and only if the function `f` tends to negative infinity along the same filter `l`. In mathematical terms, if `r < 0`, then the limit of the function `r * f(x)` as `x` approaches `l` is positive infinity if and only if the limit of `f(x)` as `x` approaches `l` is negative infinity.
More concisely: For a linearly ordered field `α`, a filter `l` over `β`, a function `f` from `β` to `α`, and a negative constant `r` of type `α`, the function `r * f(x)` approaches positive infinity along `l` if and only if `f(x)` approaches negative infinity along `l`.
|
Filter.tendsto_const_mul_atTop_iff
theorem Filter.tendsto_const_mul_atTop_iff :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [inst_1 : l.NeBot],
Filter.Tendsto (fun x => r * f x) l Filter.atTop ↔
0 < r ∧ Filter.Tendsto f l Filter.atTop ∨ r < 0 ∧ Filter.Tendsto f l Filter.atBot
This theorem states that for any types `α` and `β` where `α` is a linear ordered field, given a nontrivial filter `l` on `β`, a function `f` from `β` to `α`, and a value `r` in `α`, the function that multiplies each output of `f` by `r` tends to infinity along `l` if and only if one of the following conditions is met: either `r` is greater than zero and `f` tends to infinity along `l`, or `r` is less than zero and `f` tends to negative infinity along `l`. The "tends to infinity" and "tends to negative infinity" phrases represent the limit of the function as the input value approaches infinity or negative infinity respectively.
More concisely: For a linear ordered field `α`, a filter `l` on type `β`, and a function `f` from `β` to `α`, if `r` in `α` is either positive and `f` tends to infinity along `l`, or negative and `f` tends to negative infinity along `l`, then the function `x ↦ r * f(x)` tends to infinity (or negative infinity) along `l`.
|
Filter.map_atTop_finset_sum_le_of_sum_eq
theorem Filter.map_atTop_finset_sum_le_of_sum_eq :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid α] {f : β → α} {g : γ → α},
(∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ (u'.sum fun x => g x) = v'.sum fun b => f b) →
Filter.map (fun s => s.sum fun b => f b) Filter.atTop ≤ Filter.map (fun s => s.sum fun x => g x) Filter.atTop
The theorem `Filter.map_atTop_finset_sum_le_of_sum_eq` states that given two functions `f` and `g` mapping to the same commutative additive monoid, if for every finite set `u` there exists a finite set `v` such that for every `v'` that is a superset of `v` there exists a `u'` which is a superset of `u` and the sum of `g` over `u'` equals the sum of `f` over `v'`, then the filter at the limit towards infinity of the sum of `f` over the set is less than or equal to the filter at the limit towards infinity of the sum of `g` over the set. This theorem provides a condition to compare the limiting behaviors of the summations of `f` and `g` over increasing sets as they approach infinity.
More concisely: Given functions `f` and `g` mapping to the same commutative additive monoid, if for every finite set `u`, there exists a larger finite set `v` such that the sum of `g` over `v` equals the sum of `f` over `u` and for all larger sets `v'`, the sum of `g` over `v'` is an upper bound for the sum of `f` over any superset of `u`, then the limit of the sum of `f` over increasing sets is less than or equal to the limit of the sum of `g` over increasing sets.
|
Filter.tendsto_mul_const_atBot_iff_pos
theorem Filter.tendsto_mul_const_atBot_iff_pos :
∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [inst_1 : l.NeBot],
Filter.Tendsto f l Filter.atBot → (Filter.Tendsto (fun x => f x * r) l Filter.atBot ↔ 0 < r)
This theorem states that for any types `α` and `β`, where `α` is a linear ordered field, and given a nontrivial filter `l`, a function `f` from `β` to `α`, and a real number `r`, if the function `f` tends to negative infinity along the filter `l`, then the function `fun x ↦ f x * r` also tends to negative infinity along the same filter `l` if and only if `r` is a positive number.
More concisely: For any linear ordered field `α`, nontrivial filter `l` on `β`, function `f` from `β` to `α`, and positive real number `r`, if `f` tends to negative infinity along `l`, then `fun x ↦ f x * r` also tends to negative infinity along `l`.
|
Mathlib.Order.Filter.AtTopBot._auxLemma.16
theorem Mathlib.Order.Filter.AtTopBot._auxLemma.16 :
∀ {α : Type u_3} {β : Type u_4} [inst : OrderedAddCommGroup β] {l : Filter α} {f : α → β},
Filter.Tendsto (fun x => -f x) l Filter.atTop = Filter.Tendsto f l Filter.atBot
This theorem states that for any types `α` and `β`, where `β` is an ordered additive commutative group, and any filter `l` on `α` and function `f` mapping `α` to `β`, the function `-f` tends to `atTop` as `l` tends to infinity if and only if the function `f` tends to `atBot` as `l` tends to negative infinity. In mathematical terms, this is saying that $\lim_{x\to\infty}-f(x) = \lim_{x\to-\infty}f(x)$.
More concisely: For functions from an arbitrary type to an ordered additive commutative group, the negation of the function converges to the top element as the filter approaches infinity if and only if the original function converges to the bottom element as the filter approaches negative infinity.
|