Convergence to ±infinity in ordered rings

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

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

theorem Filter.tendsto_pow_atTop {α : Type u_1} [OrderedSemiring α] {n : ℕ} (hn : n ≠ 0) : Filter.Tendsto (fun (x : α) => x ^ n) Filter.atTop Filter.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) =ᶠ[Filter.atTop] fun (x : ℕ) => 0

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

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

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

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

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

@[simp]

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

theorem Filter.not_tendsto_pow_atTop_atBot {α : Type u_1} [LinearOrderedRing α] {n : ℕ} : ¬Filter.Tendsto (fun (x : α) => x ^ n) Filter.atTop Filter.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