Convergence to ±infinity in linear ordered (semi)fields

Multiplication by constant: iff lemmas

theorem Filter.tendsto_const_mul_atTop_of_pos {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) : Tendsto (fun (x : β) => r * f x) l atTop ↔ Tendsto f l atTop

If r is a positive constant, fun x ↦ r * f x tends to infinity along a filter if and only if f tends to infinity along the same filter.

theorem Filter.tendsto_mul_const_atTop_of_pos {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) : Tendsto (fun (x : β) => f x * r) l atTop ↔ Tendsto f l atTop

If r is a positive constant, fun x ↦ f x * r tends to infinity along a filter if and only if f tends to infinity along the same filter.

theorem Filter.tendsto_div_const_atTop_of_pos {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) : Tendsto (fun (x : β) => f x / r) l atTop ↔ Tendsto f l atTop

If r is a positive constant, x ↦ f x / r tends to infinity along a filter if and only if f tends to infinity along the same filter.

theorem Filter.tendsto_const_mul_atTop_iff_pos {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atTop) : Tendsto (fun (x : β) => r * f x) l atTop ↔ 0 < r

If f tends to infinity along a nontrivial filter l, then fun x ↦ r * f x tends to infinity if and only if 0 < r.

theorem Filter.tendsto_mul_const_atTop_iff_pos {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atTop) : Tendsto (fun (x : β) => f x * r) l atTop ↔ 0 < r

If f tends to infinity along a nontrivial filter l, then fun x ↦ f x * r tends to infinity if and only if 0 < r.

theorem Filter.tendsto_div_const_atTop_iff_pos {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atTop) : Tendsto (fun (x : β) => f x / r) l atTop ↔ 0 < r

If f tends to infinity along a nontrivial filter l, then x ↦ f x * r tends to infinity if and only if 0 < r.

theorem Filter.Tendsto.const_mul_atTop {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Tendsto f l atTop) : Tendsto (fun (x : β) => r * f x) l atTop

If f tends to infinity along a filter, then f multiplied by a positive constant (on the left) also tends to infinity. For a version working in ℕ or ℤ, use Filter.Tendsto.const_mul_atTop' instead.

theorem Filter.Tendsto.atTop_mul_const {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Tendsto f l atTop) : Tendsto (fun (x : β) => f x * r) l atTop

If a function f tends to infinity along a filter, then f multiplied by a positive constant (on the right) also tends to infinity. For a version working in ℕ or ℤ, use Filter.Tendsto.atTop_mul_const' instead.

theorem Filter.Tendsto.atTop_div_const {α : Type u_1} {β : Type u_2} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Tendsto f l atTop) : Tendsto (fun (x : β) => f x / r) l atTop

If a function f tends to infinity along a filter, then f divided by a positive constant also tends to infinity.

theorem Filter.tendsto_const_mul_pow_atTop {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {c : α} {n : ℕ} (hn : n ≠ 0) (hc : 0 < c) : Tendsto (fun (x : α) => c * x ^ n) atTop atTop

theorem Filter.tendsto_const_mul_pow_atTop_iff {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {c : α} {n : ℕ} : Tendsto (fun (x : α) => c * x ^ n) atTop atTop ↔ n ≠ 0 ∧ 0 < c

theorem Filter.tendsto_zpow_atTop_atTop {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {n : ℤ} (hn : 0 < n) : Tendsto (fun (x : α) => x ^ n) atTop atTop

theorem Filter.tendsto_const_mul_atBot_of_pos {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) : Tendsto (fun (x : β) => r * f x) l atBot ↔ Tendsto f l atBot

If r is a positive constant, fun x ↦ r * f x tends to negative infinity along a filter if and only if f tends to negative infinity along the same filter.

theorem Filter.tendsto_mul_const_atBot_of_pos {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) : Tendsto (fun (x : β) => f x * r) l atBot ↔ Tendsto f l atBot

If r is a positive constant, fun x ↦ f x * r tends to negative infinity along a filter if and only if f tends to negative infinity along the same filter.

theorem Filter.tendsto_div_const_atBot_of_pos {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) : Tendsto (fun (x : β) => f x / r) l atBot ↔ Tendsto f l atBot

If r is a positive constant, fun x ↦ f x / r tends to negative infinity along a filter if and only if f tends to negative infinity along the same filter.

theorem Filter.tendsto_const_mul_atTop_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) : Tendsto (fun (x : β) => r * f x) l atTop ↔ Tendsto f l atBot

If r is a negative constant, fun x ↦ r * f x tends to infinity along a filter l if and only if f tends to negative infinity along l.

theorem Filter.tendsto_mul_const_atTop_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) : Tendsto (fun (x : β) => f x * r) l atTop ↔ Tendsto f l atBot

If r is a negative constant, fun x ↦ f x * r tends to infinity along a filter l if and only if f tends to negative infinity along l.

theorem Filter.tendsto_div_const_atTop_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) : Tendsto (fun (x : β) => f x / r) l atTop ↔ Tendsto f l atBot

If r is a negative constant, fun x ↦ f x / r tends to infinity along a filter l if and only if f tends to negative infinity along l.

theorem Filter.tendsto_const_mul_atBot_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) : Tendsto (fun (x : β) => r * f x) l atBot ↔ Tendsto f l atTop

If r is a negative constant, fun x ↦ r * f x tends to negative infinity along a filter l if and only if f tends to infinity along l.

theorem Filter.tendsto_mul_const_atBot_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) : Tendsto (fun (x : β) => f x * r) l atBot ↔ Tendsto f l atTop

If r is a negative constant, fun x ↦ f x * r tends to negative infinity along a filter l if and only if f tends to infinity along l.

theorem Filter.tendsto_div_const_atBot_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) : Tendsto (fun (x : β) => f x / r) l atBot ↔ Tendsto f l atTop

If r is a negative constant, fun x ↦ f x / r tends to negative infinity along a filter l if and only if f tends to infinity along l.

theorem Filter.tendsto_const_mul_atTop_iff {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] : Tendsto (fun (x : β) => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

The function fun x ↦ r * f x tends to infinity along a nontrivial filter if and only if r > 0 and f tends to infinity or r < 0 and f tends to negative infinity.

theorem Filter.tendsto_mul_const_atTop_iff {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] : Tendsto (fun (x : β) => f x * r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

The function fun x ↦ f x * r tends to infinity along a nontrivial filter if and only if r > 0 and f tends to infinity or r < 0 and f tends to negative infinity.

theorem Filter.tendsto_div_const_atTop_iff {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] : Tendsto (fun (x : β) => f x / r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

The function fun x ↦ f x / r tends to infinity along a nontrivial filter if and only if r > 0 and f tends to infinity or r < 0 and f tends to negative infinity.

theorem Filter.tendsto_const_mul_atBot_iff {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] : Tendsto (fun (x : β) => r * f x) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

The function fun x ↦ r * f x tends to negative infinity along a nontrivial filter if and only if r > 0 and f tends to negative infinity or r < 0 and f tends to infinity.

theorem Filter.tendsto_mul_const_atBot_iff {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] : Tendsto (fun (x : β) => f x * r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

The function fun x ↦ f x * r tends to negative infinity along a nontrivial filter if and only if r > 0 and f tends to negative infinity or r < 0 and f tends to infinity.

theorem Filter.tendsto_div_const_atBot_iff {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] : Tendsto (fun (x : β) => f x / r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

The function fun x ↦ f x / r tends to negative infinity along a nontrivial filter if and only if r > 0 and f tends to negative infinity or r < 0 and f tends to infinity.

theorem Filter.tendsto_const_mul_atTop_iff_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atBot) : Tendsto (fun (x : β) => r * f x) l atTop ↔ r < 0

If f tends to negative infinity along a nontrivial filter l, then fun x ↦ r * f x tends to infinity if and only if r < 0.

theorem Filter.tendsto_mul_const_atTop_iff_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atBot) : Tendsto (fun (x : β) => f x * r) l atTop ↔ r < 0

If f tends to negative infinity along a nontrivial filter l, then fun x ↦ f x * r tends to infinity if and only if r < 0.

theorem Filter.tendsto_div_const_atTop_iff_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atBot) : Tendsto (fun (x : β) => f x / r) l atTop ↔ r < 0

If f tends to negative infinity along a nontrivial filter l, then fun x ↦ f x / r tends to infinity if and only if r < 0.

theorem Filter.tendsto_const_mul_atBot_iff_pos {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atBot) : Tendsto (fun (x : β) => r * f x) l atBot ↔ 0 < r

If f tends to negative infinity along a nontrivial filter l, then fun x ↦ r * f x tends to negative infinity if and only if 0 < r.

theorem Filter.tendsto_mul_const_atBot_iff_pos {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atBot) : Tendsto (fun (x : β) => f x * r) l atBot ↔ 0 < r

If f tends to negative infinity along a nontrivial filter l, then fun x ↦ f x * r tends to negative infinity if and only if 0 < r.

theorem Filter.tendsto_div_const_atBot_iff_pos {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atBot) : Tendsto (fun (x : β) => f x / r) l atBot ↔ 0 < r

If f tends to negative infinity along a nontrivial filter l, then fun x ↦ f x / r tends to negative infinity if and only if 0 < r.

theorem Filter.tendsto_const_mul_atBot_iff_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atTop) : Tendsto (fun (x : β) => r * f x) l atBot ↔ r < 0

If f tends to infinity along a nontrivial filter, fun x ↦ r * f x tends to negative infinity if and only if r < 0.

theorem Filter.tendsto_mul_const_atBot_iff_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atTop) : Tendsto (fun (x : β) => f x * r) l atBot ↔ r < 0

If f tends to infinity along a nontrivial filter, fun x ↦ f x * r tends to negative infinity if and only if r < 0.

theorem Filter.tendsto_div_const_atBot_iff_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Tendsto f l atTop) : Tendsto (fun (x : β) => f x / r) l atBot ↔ r < 0

If f tends to infinity along a nontrivial filter, fun x ↦ f x / r tends to negative infinity if and only if r < 0.

theorem Filter.Tendsto.const_mul_atTop_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Tendsto f l atTop) : Tendsto (fun (x : β) => r * f x) l atBot

If a function f tends to infinity along a filter, then f multiplied by a negative constant (on the left) tends to negative infinity.

theorem Filter.Tendsto.atTop_mul_const_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Tendsto f l atTop) : Tendsto (fun (x : β) => f x * r) l atBot

If a function f tends to infinity along a filter, then f multiplied by a negative constant (on the right) tends to negative infinity.

theorem Filter.Tendsto.atTop_div_const_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Tendsto f l atTop) : Tendsto (fun (x : β) => f x / r) l atBot

If a function f tends to infinity along a filter, then f divided by a negative constant tends to negative infinity.

theorem Filter.Tendsto.const_mul_atBot {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Tendsto f l atBot) : Tendsto (fun (x : β) => r * f x) l atBot

If a function f tends to negative infinity along a filter, then f multiplied by a positive constant (on the left) also tends to negative infinity.

theorem Filter.Tendsto.atBot_mul_const {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Tendsto f l atBot) : Tendsto (fun (x : β) => f x * r) l atBot

If a function f tends to negative infinity along a filter, then f multiplied by a positive constant (on the right) also tends to negative infinity.

theorem Filter.Tendsto.atBot_div_const {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Tendsto f l atBot) : Tendsto (fun (x : β) => f x / r) l atBot

If a function f tends to negative infinity along a filter, then f divided by a positive constant also tends to negative infinity.

theorem Filter.Tendsto.const_mul_atBot_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Tendsto f l atBot) : Tendsto (fun (x : β) => r * f x) l atTop

If a function f tends to negative infinity along a filter, then f multiplied by a negative constant (on the left) tends to positive infinity.

theorem Filter.Tendsto.atBot_mul_const_of_neg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Tendsto f l atBot) : Tendsto (fun (x : β) => f x * r) l atTop

If a function tends to negative infinity along a filter, then f multiplied by a negative constant (on the right) tends to positive infinity.

theorem Filter.tendsto_neg_const_mul_pow_atTop {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {c : α} {n : ℕ} (hn : n ≠ 0) (hc : c < 0) : Tendsto (fun (x : α) => c * x ^ n) atTop atBot

theorem Filter.tendsto_const_mul_pow_atBot_iff {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {c : α} {n : ℕ} : Tendsto (fun (x : α) => c * x ^ n) atTop atBot ↔ n ≠ 0 ∧ c < 0