Filter.Tendsto.atTop_mul_const'
theorem Filter.Tendsto.atTop_mul_const' :
∀ {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [inst : LinearOrderedSemiring R]
[inst_1 : Archimedean 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 linearly ordered semiring `R` with the archimedean property, any filter `l` on a type `α`, and any function `f` from `α` to `R`, if `f` tends to infinity along `l`, then the function obtained by multiplying `f` by a positive constant `r` also tends to infinity along `l`. This theorem is valid in various mathematical structures such as natural numbers, integers, and real numbers due to the archimedean assumption.
More concisely: If `f` tends to infinity along filter `l` in a linearly ordered semiring `R` with the archimedean property, then the function `rf` obtained by multiplying `f` by a positive constant `r` also tends to infinity along `l`.
|
Filter.Tendsto.atBot_mul_neg_const'
theorem Filter.Tendsto.atBot_mul_neg_const' :
∀ {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [inst : LinearOrderedRing R]
[inst_1 : Archimedean 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 type `α`, type `R` which is a linearly ordered ring, a filter `l` on `α`, a function `f` from `α` to `R`, and a real number `r`, if `r` is less than zero and if the function `f` tends to negative infinity at the filter `l`, then the function which maps `x` to the product of `f(x)` and `r` tends to positive infinity at the filter `l`. This theorem requires the `Archimedean` property of the ring `R`. There is another version of this theorem for `LinearOrderedField`s which doesn't require the `Archimedean` property.
More concisely: For any type `α`, linearly ordered ring `R` with the Archimedean property, filter `l` on `α`, function `f` from `α` to `R`, and real number `r < 0`, if `f(x)` approaches negative infinity as `x` approaches elements in the filter `l`, then the function `x => r * f(x)` approaches positive infinity as `x` approaches elements in the filter `l`.
|
Filter.Tendsto.atBot_mul_const'
theorem Filter.Tendsto.atBot_mul_const' :
∀ {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [inst : LinearOrderedRing R]
[inst_1 : Archimedean R],
0 < r → Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => f x * r) l Filter.atBot
This theorem states that for any types `α` and `R`, any filter `l` on `α`, any function `f` from `α` to `R`, and any real number `r` satisfying 0 < r, given that `R` is a linear ordered ring and `R` is Archimedean, if the function `f` tends to negative infinity (as defined by the `atBot` filter) as its input values approach the values described by the filter `l`, then the function that multiplies the output of `f` by `r` also tends to negative infinity as its input values approach the values described by the same filter `l`. This is a variant of the theorem `Filter.Tendsto.atBot_mul_const` for linear ordered fields, but with an additional requirement that `R` is Archimedean.
More concisely: If `α` is a type, `l` is a filter on `α`, `R` is a linear ordered ring and Archimedean, `f : α → R`, and `r` is a positive real number, then `atBot l` implies `atBot (λx : α, r * f x)`.
|
Filter.Tendsto.const_mul_atTop'
theorem Filter.Tendsto.const_mul_atTop' :
∀ {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [inst : LinearOrderedSemiring R]
[inst_1 : Archimedean R],
0 < r → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => r * f x) l Filter.atTop
This theorem states that if a function `f` tends to infinity as its input approaches some limit within a filter `l`, then the function multiplied by a positive constant `r` also tends to infinity as its input approaches the same limit. Here, the function `f` is from some type `α` to some type `R`, the constant `r` is of type `R`, and `R` is assumed to be a linear ordered semiring and Archimedean. This theorem is applicable to the natural numbers `ℕ`, integers `ℤ`, and real numbers `ℝ`. The Archimedean property is not necessary for the theorem, but it makes the theorem applicable to these types. Note that a similar theorem for ordered fields is given in `Filter.Tendsto.const_mul_atTop`.
More concisely: If a function `f : α → R` tends to infinity in a filter `l` as its input approaches some limit, then the function `rf : α → R` with `rf(x) := r * f(x)` also tends to infinity in the same filter `l`.
|
Int.comap_cast_atTop
theorem Int.comap_cast_atTop :
∀ {R : Type u_2} [inst : StrictOrderedRing R] [inst_1 : Archimedean R],
Filter.comap Int.cast Filter.atTop = Filter.atTop
The theorem `Int.comap_cast_atTop` states that for any strict ordered ring `R` that is also Archimedean, the preimage (comap) of the filter `atTop` (representing the limit going to infinity) under the canonical homomorphism `Int.cast` from the integers `ℤ` to `R` is also `atTop`. In other words, in such a mathematical structure, casting integers to `R` and then considering sequences going to infinity behaves the same as considering sequences of integers going to infinity.
More concisely: For any Archimedean strict ordered ring R, the preimage of the filter atTop under Int.cast from ℤ is equal to atTop.
|
Filter.Tendsto.atTop_zsmul_const
theorem Filter.Tendsto.atTop_zsmul_const :
∀ {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [inst : LinearOrderedAddCommGroup R] [inst_1 : Archimedean R]
{f : α → ℤ}, 0 < r → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x • r) l Filter.atTop
The theorem `Filter.Tendsto.atTop_zsmul_const` states that for any types `α` and `R`, a filter `l` on `α`, an integer-valued function `f` from `α` to `ℤ`, and a constant `r` in a linearly ordered additive commutative group `R` that is also Archimedean, if `r` is positive and `f` tends to infinity with respect to `l` (i.e., for any `ℤ` that is greater than a certain value, there exists an element in the filter such that `f` of that element is greater than that `ℤ`), then `f` scaled by `r` (i.e., the function `x ↦ f(x) * r`) also tends to infinity with respect to `l`. This essentially means that multiplying a function that tends to infinity by a positive constant does not change its limit behavior.
More concisely: If `f` is a function from a filter `l` on type `α` to `ℤ` that tends to infinity with respect to `l`, and `r` is a positive constant in an Archimedean, additively commutative group `R`, then the function `x ↦ f(x) * r` also tends to infinity with respect to `l`.
|
Filter.Tendsto.atTop_mul_neg_const'
theorem Filter.Tendsto.atTop_mul_neg_const' :
∀ {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [inst : LinearOrderedRing R]
[inst_1 : Archimedean R],
r < 0 → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x * r) l Filter.atBot
This theorem states that for any types `α` and `R`, a filter `l` on `α`, a function `f` from `α` to `R`, and a real number `r`, given that `R` is a linearly ordered ring and also Archimedean, if `r` is less than zero and the function `f` tends towards infinity (i.e., `Filter.Tendsto f l Filter.atTop`), then the function obtained by multiplying `f` by `r` will tend towards negative infinity (i.e., `Filter.Tendsto (fun x => f x * r) l Filter.atBot`). In terms of calculus, this indicates that if a function approaches infinity and we multiply it by a negative constant, the result will approach negative infinity.
More concisely: If `f` tends towards infinity over filter `l` in the Archimedean, linearly ordered ring `R`, then `f * r` tends towards negative infinity over `l` for any negative real number `r`.
|