# Convergence to ±infinity in ordered rings #

source
theorem Filter.Tendsto.atTop_mul_atTop₀ {α : Type u_1} {β : Type u_2} [Semiring α] [PartialOrder α] [IsOrderedRing α] {l : Filter β} {f g : β → α} (hf : Tendsto f l atTop) (hg : Tendsto g l atTop) :
Tendsto (fun (x : β) => f x * g x) l atTop
source
theorem Filter.tendsto_mul_self_atTop {α : Type u_1} [Semiring α] [PartialOrder α] [IsOrderedRing α] :
Tendsto (fun (x : α) => x * x) atTop atTop
source
theorem Filter.tendsto_pow_atTop {α : Type u_1} [Semiring α] [PartialOrder α] [IsOrderedRing α] {n : ℕ} (hn : n ≠ 0) :
Tendsto (fun (x : α) => x ^ n) atTop atTop

The monomial function `x^n` tends to `+∞` at `+∞` for any positive natural `n`. A version for positive real powers exists as `tendsto_rpow_atTop`.

source
theorem Filter.zero_pow_eventuallyEq {α : Type u_1} [MonoidWithZero α] :
(fun (n : ℕ) => 0 ^ n) =ᶠ[atTop] fun (x : ℕ) => 0
source
theorem Filter.Tendsto.atTop_mul_atBot₀ {α : Type u_1} {β : Type u_2} [Ring α] [PartialOrder α] [IsOrderedRing α] {l : Filter β} {f g : β → α} (hf : Tendsto f l atTop) (hg : Tendsto g l atBot) :
Tendsto (fun (x : β) => f x * g x) l atBot
source
theorem Filter.Tendsto.atBot_mul_atTop₀ {α : Type u_1} {β : Type u_2} [Ring α] [PartialOrder α] [IsOrderedRing α] {l : Filter β} {f g : β → α} (hf : Tendsto f l atBot) (hg : Tendsto g l atTop) :
Tendsto (fun (x : β) => f x * g x) l atBot
source
theorem Filter.Tendsto.atBot_mul_atBot₀ {α : Type u_1} {β : Type u_2} [Ring α] [PartialOrder α] [IsOrderedRing α] {l : Filter β} {f g : β → α} (hf : Tendsto f l atBot) (hg : Tendsto g l atBot) :
Tendsto (fun (x : β) => f x * g x) l atTop
source
theorem Filter.Tendsto.atTop_of_const_mul₀ {α : Type u_1} {β : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {c : α} (hc : 0 < c) (hf : Tendsto (fun (x : β) => c * f x) l atTop) :
Tendsto f l atTop
source
theorem Filter.Tendsto.atTop_of_mul_const₀ {α : Type u_1} {β : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {c : α} (hc : 0 < c) (hf : Tendsto (fun (x : β) => f x * c) l atTop) :
Tendsto f l atTop
source
@[simp]
theorem Filter.tendsto_pow_atTop_iff {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] {n : ℕ} :
Tendsto (fun (x : α) => x ^ n) atTop atTop ↔ n ≠ 0
source
theorem Filter.not_tendsto_pow_atTop_atBot {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {n : ℕ} :
¬Tendsto (fun (x : α) => x ^ n) atTop atBot
source
theorem exists_lt_mul_self {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] (a : R) :
∃ x ≥ 0, a < x * x
source
theorem exists_le_mul_self {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] (a : R) :
∃ x ≥ 0, a ≤ x * x