Convergence to ±infinity in ordered rings

theorem Filter.Tendsto.atTop_mul_atTop {α : Type u_1} {β : Type u_2} [OrderedSemiring α] {l : Filter β} {f g : β → α} (hf : Tendsto f l atTop) (hg : Tendsto g l atTop) : Tendsto (fun (x : β) => f x * g x) l atTop

theorem Filter.tendsto_mul_self_atTop {α : Type u_1} [OrderedSemiring α] : Tendsto (fun (x : α) => x * x) atTop atTop

theorem Filter.tendsto_pow_atTop {α : Type u_1} [OrderedSemiring α] {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.

theorem Filter.zero_pow_eventuallyEq {α : Type u_1} [MonoidWithZero α] : (fun (n : ℕ) => 0 ^ n) =ᶠ[atTop] fun (x : ℕ) => 0

theorem Filter.Tendsto.atTop_mul_atBot {α : Type u_1} {β : Type u_2} [OrderedRing α] {l : Filter β} {f g : β → α} (hf : Tendsto f l atTop) (hg : Tendsto g l atBot) : Tendsto (fun (x : β) => f x * g x) l atBot

theorem Filter.Tendsto.atBot_mul_atTop {α : Type u_1} {β : Type u_2} [OrderedRing α] {l : Filter β} {f g : β → α} (hf : Tendsto f l atBot) (hg : Tendsto g l atTop) : Tendsto (fun (x : β) => f x * g x) l atBot

theorem Filter.Tendsto.atBot_mul_atBot {α : Type u_1} {β : Type u_2} [OrderedRing α] {l : Filter β} {f g : β → α} (hf : Tendsto f l atBot) (hg : Tendsto g l atBot) : Tendsto (fun (x : β) => f x * g x) l atTop

theorem Filter.Tendsto.atTop_of_const_mul {α : Type u_1} {β : Type u_2} [LinearOrderedSemiring α] {l : Filter β} {f : β → α} {c : α} (hc : 0 < c) (hf : Tendsto (fun (x : β) => c * f x) l atTop) : Tendsto f l atTop

theorem Filter.Tendsto.atTop_of_mul_const {α : Type u_1} {β : Type u_2} [LinearOrderedSemiring α] {l : Filter β} {f : β → α} {c : α} (hc : 0 < c) (hf : Tendsto (fun (x : β) => f x * c) l atTop) : Tendsto f l atTop

@[simp]

theorem Filter.tendsto_pow_atTop_iff {α : Type u_1} [LinearOrderedSemiring α] {n : ℕ} : Tendsto (fun (x : α) => x ^ n) atTop atTop ↔ n ≠ 0

theorem Filter.not_tendsto_pow_atTop_atBot {α : Type u_1} [LinearOrderedRing α] {n : ℕ} : ¬Tendsto (fun (x : α) => x ^ n) atTop atBot

theorem exists_lt_mul_self {R : Type u_3} [LinearOrderedSemiring R] (a : R) : ∃ x ≥ 0, a < x * x

theorem exists_le_mul_self {R : Type u_3} [LinearOrderedSemiring R] (a : R) : ∃ x ≥ 0, a ≤ x * x