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} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) :

Filter.Tendsto (fun (x : β) => r * f x) l Filter.atTop ↔ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_mul_const_atTop_of_pos {α : Type u_1} {β : Type u_2} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) :

Filter.Tendsto (fun (x : β) => f x * r) l Filter.atTop ↔ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_div_const_atTop_of_pos {α : Type u_1} {β : Type u_2} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) :

Filter.Tendsto (fun (x : β) => f x / r) l Filter.atTop ↔ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_const_mul_atTop_iff_pos {α : Type u_1} {β : Type u_2} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Filter.Tendsto f l Filter.atTop) :

Filter.Tendsto (fun (x : β) => r * f x) l Filter.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.

source

theorem Filter.tendsto_mul_const_atTop_iff_pos {α : Type u_1} {β : Type u_2} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Filter.Tendsto f l Filter.atTop) :

Filter.Tendsto (fun (x : β) => f x * r) l Filter.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.

source

theorem Filter.tendsto_div_const_atTop_iff_pos {α : Type u_1} {β : Type u_2} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Filter.Tendsto f l Filter.atTop) :

Filter.Tendsto (fun (x : β) => f x / r) l Filter.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.

source

theorem Filter.Tendsto.const_mul_atTop {α : Type u_1} {β : Type u_2} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atTop) :

Filter.Tendsto (fun (x : β) => r * f x) l Filter.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.

source

theorem Filter.Tendsto.atTop_mul_const {α : Type u_1} {β : Type u_2} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atTop) :

Filter.Tendsto (fun (x : β) => f x * r) l Filter.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.

source

theorem Filter.Tendsto.atTop_div_const {α : Type u_1} {β : Type u_2} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atTop) :

Filter.Tendsto (fun (x : β) => f x / r) l Filter.atTop

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

source

theorem Filter.tendsto_const_mul_pow_atTop {α : Type u_1} [LinearOrderedSemifield α] {c : α} {n : ℕ} (hn : n ≠ 0) (hc : 0 < c) :

Filter.Tendsto (fun (x : α) => c * x ^ n) Filter.atTop Filter.atTop

source

theorem Filter.tendsto_const_mul_pow_atTop_iff {α : Type u_1} [LinearOrderedSemifield α] {c : α} {n : ℕ} :

Filter.Tendsto (fun (x : α) => c * x ^ n) Filter.atTop Filter.atTop ↔ n ≠ 0 ∧ 0 < c

source

theorem Filter.tendsto_zpow_atTop_atTop {α : Type u_1} [LinearOrderedSemifield α] {n : ℤ} (hn : 0 < n) :

Filter.Tendsto (fun (x : α) => x ^ n) Filter.atTop Filter.atTop

source

theorem Filter.tendsto_const_mul_atBot_of_pos {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) :

Filter.Tendsto (fun (x : β) => r * f x) l Filter.atBot ↔ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_mul_const_atBot_of_pos {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) :

Filter.Tendsto (fun (x : β) => f x * r) l Filter.atBot ↔ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_div_const_atBot_of_pos {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) :

Filter.Tendsto (fun (x : β) => f x / r) l Filter.atBot ↔ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_const_mul_atTop_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) :

Filter.Tendsto (fun (x : β) => r * f x) l Filter.atTop ↔ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_mul_const_atTop_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) :

Filter.Tendsto (fun (x : β) => f x * r) l Filter.atTop ↔ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_div_const_atTop_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) :

Filter.Tendsto (fun (x : β) => f x / r) l Filter.atTop ↔ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_const_mul_atBot_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) :

Filter.Tendsto (fun (x : β) => r * f x) l Filter.atBot ↔ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_mul_const_atBot_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) :

Filter.Tendsto (fun (x : β) => f x * r) l Filter.atBot ↔ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_div_const_atBot_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) :

Filter.Tendsto (fun (x : β) => f x / r) l Filter.atBot ↔ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_const_mul_atTop_iff {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] :

Filter.Tendsto (fun (x : β) => r * f x) l Filter.atTop ↔ 0 < r ∧ Filter.Tendsto f l Filter.atTop ∨ r < 0 ∧ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_mul_const_atTop_iff {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] :

Filter.Tendsto (fun (x : β) => f x * r) l Filter.atTop ↔ 0 < r ∧ Filter.Tendsto f l Filter.atTop ∨ r < 0 ∧ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_div_const_atTop_iff {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] :

Filter.Tendsto (fun (x : β) => f x / r) l Filter.atTop ↔ 0 < r ∧ Filter.Tendsto f l Filter.atTop ∨ r < 0 ∧ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_const_mul_atBot_iff {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] :

Filter.Tendsto (fun (x : β) => r * f x) l Filter.atBot ↔ 0 < r ∧ Filter.Tendsto f l Filter.atBot ∨ r < 0 ∧ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_mul_const_atBot_iff {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] :

Filter.Tendsto (fun (x : β) => f x * r) l Filter.atBot ↔ 0 < r ∧ Filter.Tendsto f l Filter.atBot ∨ r < 0 ∧ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_div_const_atBot_iff {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] :

Filter.Tendsto (fun (x : β) => f x / r) l Filter.atBot ↔ 0 < r ∧ Filter.Tendsto f l Filter.atBot ∨ r < 0 ∧ Filter.Tendsto f l Filter.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.

source

theorem Filter.tendsto_const_mul_atTop_iff_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Filter.Tendsto f l Filter.atBot) :

Filter.Tendsto (fun (x : β) => r * f x) l Filter.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.

source

theorem Filter.tendsto_mul_const_atTop_iff_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Filter.Tendsto f l Filter.atBot) :

Filter.Tendsto (fun (x : β) => f x * r) l Filter.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.

source

theorem Filter.tendsto_div_const_atTop_iff_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Filter.Tendsto f l Filter.atBot) :

Filter.Tendsto (fun (x : β) => f x / r) l Filter.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.

source

theorem Filter.tendsto_const_mul_atBot_iff_pos {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Filter.Tendsto f l Filter.atBot) :

Filter.Tendsto (fun (x : β) => r * f x) l Filter.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.

source

theorem Filter.tendsto_mul_const_atBot_iff_pos {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Filter.Tendsto f l Filter.atBot) :

Filter.Tendsto (fun (x : β) => f x * r) l Filter.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.

source

theorem Filter.tendsto_div_const_atBot_iff_pos {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Filter.Tendsto f l Filter.atBot) :

Filter.Tendsto (fun (x : β) => f x / r) l Filter.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.

source

theorem Filter.tendsto_const_mul_atBot_iff_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Filter.Tendsto f l Filter.atTop) :

Filter.Tendsto (fun (x : β) => r * f x) l Filter.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.

source

theorem Filter.tendsto_mul_const_atBot_iff_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Filter.Tendsto f l Filter.atTop) :

Filter.Tendsto (fun (x : β) => f x * r) l Filter.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.

source

theorem Filter.tendsto_div_const_atBot_iff_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [l.NeBot] (h : Filter.Tendsto f l Filter.atTop) :

Filter.Tendsto (fun (x : β) => f x / r) l Filter.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.

source

theorem Filter.Tendsto.const_mul_atTop_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Filter.Tendsto f l Filter.atTop) :

Filter.Tendsto (fun (x : β) => r * f x) l Filter.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.

source

theorem Filter.Tendsto.atTop_mul_const_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Filter.Tendsto f l Filter.atTop) :

Filter.Tendsto (fun (x : β) => f x * r) l Filter.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.

source

theorem Filter.Tendsto.atTop_div_const_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Filter.Tendsto f l Filter.atTop) :

Filter.Tendsto (fun (x : β) => f x / r) l Filter.atBot

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

source

theorem Filter.Tendsto.const_mul_atBot {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atBot) :

Filter.Tendsto (fun (x : β) => r * f x) l Filter.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.

source

theorem Filter.Tendsto.atBot_mul_const {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atBot) :

Filter.Tendsto (fun (x : β) => f x * r) l Filter.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.

source

theorem Filter.Tendsto.atBot_div_const {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atBot) :

Filter.Tendsto (fun (x : β) => f x / r) l Filter.atBot

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

source

theorem Filter.Tendsto.const_mul_atBot_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Filter.Tendsto f l Filter.atBot) :

Filter.Tendsto (fun (x : β) => r * f x) l Filter.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.

source

theorem Filter.Tendsto.atBot_mul_const_of_neg {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Filter.Tendsto f l Filter.atBot) :

Filter.Tendsto (fun (x : β) => f x * r) l Filter.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.

source

theorem Filter.tendsto_neg_const_mul_pow_atTop {α : Type u_1} [LinearOrderedField α] {c : α} {n : ℕ} (hn : n ≠ 0) (hc : c < 0) :

Filter.Tendsto (fun (x : α) => c * x ^ n) Filter.atTop Filter.atBot

source

theorem Filter.tendsto_const_mul_pow_atBot_iff {α : Type u_1} [LinearOrderedField α] {c : α} {n : ℕ} :

Filter.Tendsto (fun (x : α) => c * x ^ n) Filter.atTop Filter.atBot ↔ n ≠ 0 ∧ c < 0

source

@[deprecated Filter.Tendsto.const_mul_atTop_of_neg]

theorem Filter.Tendsto.neg_const_mul_atTop {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Filter.Tendsto f l Filter.atTop) :

Filter.Tendsto (fun (x : β) => r * f x) l Filter.atBot

Alias of Filter.Tendsto.const_mul_atTop_of_neg.

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

source

@[deprecated Filter.Tendsto.atTop_mul_const_of_neg]

theorem Filter.Tendsto.atTop_mul_neg_const {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Filter.Tendsto f l Filter.atTop) :

Filter.Tendsto (fun (x : β) => f x * r) l Filter.atBot

Alias of Filter.Tendsto.atTop_mul_const_of_neg.

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

source

@[deprecated Filter.Tendsto.const_mul_atBot_of_neg]

theorem Filter.Tendsto.neg_const_mul_atBot {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Filter.Tendsto f l Filter.atBot) :

Filter.Tendsto (fun (x : β) => r * f x) l Filter.atTop

Alias of Filter.Tendsto.const_mul_atBot_of_neg.

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.

source

@[deprecated Filter.Tendsto.atBot_mul_const_of_neg]

theorem Filter.Tendsto.atBot_mul_neg_const {α : Type u_1} {β : Type u_2} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Filter.Tendsto f l Filter.atBot) :

Filter.Tendsto (fun (x : β) => f x * r) l Filter.atTop

Alias of Filter.Tendsto.atBot_mul_const_of_neg.

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

HepLean Documentation

Mathlib.Order.Filter.AtTopBot.Field

Convergence to ±infinity in linear ordered (semi)fields #

Multiplication by constant: iff lemmas #