doc-next-gen

Mathlib.Order.Filter.AtTopBot.Field

Module docstring

{"# Convergence to ±infinity in linear ordered (semi)fields ","### Multiplication by constant: iff lemmas "}

Filter.tendsto_const_mul_atTop_of_pos theorem
(hr : 0 < r) : Tendsto (fun x => r * f x) l atTop ↔ Tendsto f l atTop
Full source 
/-- 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 tendsto_const_mul_atTop_of_pos (hr : 0 < r) :
    TendstoTendsto (fun x => r * f x) l atTop ↔ Tendsto f l atTop :=
  ⟨fun h => h.atTop_of_const_mul₀ hr, fun h =>
    Tendsto.atTop_of_const_mul₀ (inv_pos.2 hr) <| by simpa only [inv_mul_cancel_left₀ hr.ne'] ⟩
Multiplication by Positive Constant Preserves Tendency to Infinity
Informal description
Let $r$ be a positive real number and $f$ be a function. Then the function $x \mapsto r \cdot f(x)$ tends to infinity along a filter $l$ if and only if $f$ tends to infinity along the same filter $l$.
Filter.tendsto_mul_const_atTop_of_pos theorem
(hr : 0 < r) : Tendsto (fun x => f x * r) l atTop ↔ Tendsto f l atTop
Full source 
/-- 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 tendsto_mul_const_atTop_of_pos (hr : 0 < r) :
    TendstoTendsto (fun x => f x * r) l atTop ↔ Tendsto f l atTop := by
  simpa only [mul_comm] using tendsto_const_mul_atTop_of_pos hr
Right Multiplication by Positive Constant Preserves Tendency to Infinity
Informal description
Let $r$ be a positive real number and $f$ be a function. Then the function $x \mapsto f(x) \cdot r$ tends to infinity along a filter $l$ if and only if $f$ tends to infinity along the same filter $l$.
Filter.tendsto_div_const_atTop_of_pos theorem
(hr : 0 < r) : Tendsto (fun x ↦ f x / r) l atTop ↔ Tendsto f l atTop
Full source 
/-- 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. -/
lemma tendsto_div_const_atTop_of_pos (hr : 0 < r) :
    TendstoTendsto (fun x ↦ f x / r) l atTop ↔ Tendsto f l atTop := by
  simpa only [div_eq_mul_inv] using tendsto_mul_const_atTop_of_pos (inv_pos.2 hr)
Division by Positive Constant Preserves Tendency to Infinity
Informal description
Let $r$ be a positive real number and $f$ be a function. Then the function $x \mapsto f(x) / r$ tends to infinity along a filter $l$ if and only if $f$ tends to infinity along the same filter $l$.
Filter.tendsto_const_mul_atTop_iff_pos theorem
[NeBot l] (h : Tendsto f l atTop) : Tendsto (fun x => r * f x) l atTop ↔ 0 < r
Full source 
/-- 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 tendsto_const_mul_atTop_iff_pos [NeBot l] (h : Tendsto f l atTop) :
    TendstoTendsto (fun x => r * f x) l atTop ↔ 0 < r := by
  refine ⟨fun hrf => not_le.mp fun hr => ?_, fun hr => (tendsto_const_mul_atTop_of_pos hr).mpr h⟩
  rcases ((h.eventually_ge_atTop 0).and (hrf.eventually_gt_atTop 0)).exists with ⟨x, hx, hrx⟩
  exact (mul_nonpos_of_nonpos_of_nonneg hr hx).not_lt hrx
Multiplication by Constant Preserves Tendency to Infinity iff Positive
Informal description
Let $l$ be a nontrivial filter and $f$ a function such that $f$ tends to infinity along $l$. Then the function $x \mapsto r \cdot f(x)$ tends to infinity along $l$ if and only if $r > 0$.
Filter.tendsto_mul_const_atTop_iff_pos theorem
[NeBot l] (h : Tendsto f l atTop) : Tendsto (fun x => f x * r) l atTop ↔ 0 < r
Full source 
/-- 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 tendsto_mul_const_atTop_iff_pos [NeBot l] (h : Tendsto f l atTop) :
    TendstoTendsto (fun x => f x * r) l atTop ↔ 0 < r := by
  simp only [mul_comm _ r, tendsto_const_mul_atTop_iff_pos h]
Right Multiplication by Constant Preserves Tendency to Infinity iff Positive
Informal description
Let $l$ be a nontrivial filter and $f$ a function such that $f$ tends to infinity along $l$. Then the function $x \mapsto f(x) \cdot r$ tends to infinity along $l$ if and only if $r > 0$.
Filter.tendsto_div_const_atTop_iff_pos theorem
[NeBot l] (h : Tendsto f l atTop) : Tendsto (fun x ↦ f x / r) l atTop ↔ 0 < r
Full source 
/-- If `f` tends to infinity along a nontrivial filter `l`, then
`x ↦ f x * r` tends to infinity if and only if `0 < r`. -/
lemma tendsto_div_const_atTop_iff_pos [NeBot l] (h : Tendsto f l atTop) :
    TendstoTendsto (fun x ↦ f x / r) l atTop ↔ 0 < r := by
  simp only [div_eq_mul_inv, tendsto_mul_const_atTop_iff_pos h, inv_pos]
Division by Constant Preserves Tendency to Infinity iff Positive
Informal description
Let $l$ be a nontrivial filter and $f$ a function such that $f$ tends to infinity along $l$. Then the function $x \mapsto f(x) / r$ tends to infinity along $l$ if and only if $r > 0$.
Filter.Tendsto.const_mul_atTop theorem
(hr : 0 < r) (hf : Tendsto f l atTop) : Tendsto (fun x => r * f x) l atTop
Full source 
/-- 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 Tendsto.const_mul_atTop (hr : 0 < r) (hf : Tendsto f l atTop) :
    Tendsto (fun x => r * f x) l atTop :=
  (tendsto_const_mul_atTop_of_pos hr).2 hf
Multiplication by Positive Constant Preserves Tendency to Infinity
Informal description
Let $r$ be a positive real number and $f$ be a function. If $f$ tends to infinity along a filter $l$, then the function $x \mapsto r \cdot f(x)$ also tends to infinity along the same filter $l$.
Filter.Tendsto.atTop_mul_const theorem
(hr : 0 < r) (hf : Tendsto f l atTop) : Tendsto (fun x => f x * r) l atTop
Full source 
/-- 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 Tendsto.atTop_mul_const (hr : 0 < r) (hf : Tendsto f l atTop) :
    Tendsto (fun x => f x * r) l atTop :=
  (tendsto_mul_const_atTop_of_pos hr).2 hf
Right Multiplication by Positive Constant Preserves Tendency to Infinity
Informal description
Let $f$ be a function and $l$ a filter. If $f$ tends to infinity along $l$ and $r$ is a positive real number, then the function $x \mapsto f(x) \cdot r$ also tends to infinity along $l$.
Filter.Tendsto.atTop_div_const theorem
(hr : 0 < r) (hf : Tendsto f l atTop) : Tendsto (fun x => f x / r) l atTop
Full source 
/-- If a function `f` tends to infinity along a filter, then `f` divided by a positive
constant also tends to infinity. -/
theorem Tendsto.atTop_div_const (hr : 0 < r) (hf : Tendsto f l atTop) :
    Tendsto (fun x => f x / r) l atTop := by
  simpa only [div_eq_mul_inv] using hf.atTop_mul_const (inv_pos.2 hr)
Division by Positive Constant Preserves Tendency to Infinity
Informal description
Let $f$ be a function and $l$ a filter. If $f$ tends to infinity along $l$ and $r$ is a positive real number, then the function $x \mapsto f(x) / r$ also tends to infinity along $l$.
Filter.tendsto_const_mul_pow_atTop theorem
(hn : n ≠ 0) (hc : 0 < c) : Tendsto (fun x => c * x ^ n) atTop atTop
Full source 
theorem tendsto_const_mul_pow_atTop (hn : n ≠ 0) (hc : 0 < c) :
    Tendsto (fun x => c * x ^ n) atTop atTop :=
  Tendsto.const_mul_atTop hc (tendsto_pow_atTop hn)
Polynomial Growth to Infinity: $c x^n \to +\infty$ as $x \to +\infty$ for $c > 0$ and $n \neq 0$
Informal description
Let $c$ be a positive real number and $n$ be a nonzero natural number. Then the function $x \mapsto c \cdot x^n$ tends to $+\infty$ as $x$ tends to $+\infty$.
Filter.tendsto_const_mul_pow_atTop_iff theorem
: Tendsto (fun x => c * x ^ n) atTop atTop ↔ n ≠ 0 ∧ 0 < c
Full source 
theorem tendsto_const_mul_pow_atTop_iff :
    TendstoTendsto (fun x => c * x ^ n) atTop atTop ↔ n ≠ 0 ∧ 0 < c := by
  refine ⟨fun h => ⟨?_, ?_⟩, fun h => tendsto_const_mul_pow_atTop h.1 h.2⟩
  · rintro rfl
    simp only [pow_zero, not_tendsto_const_atTop] at h
  · rcases ((h.eventually_gt_atTop 0).and (eventually_ge_atTop 0)).exists with ⟨k, hck, hk⟩
    exact pos_of_mul_pos_left hck (pow_nonneg hk _)
Characterization of Polynomial Growth to Infinity: $c x^n \to +\infty$ iff $n \neq 0$ and $c > 0$
Informal description
For a function of the form $x \mapsto c \cdot x^n$ where $c$ is a constant and $n$ is an exponent, the function tends to $+\infty$ as $x$ tends to $+\infty$ if and only if $n$ is nonzero and $c$ is positive.
Filter.tendsto_zpow_atTop_atTop theorem
{n : ℤ} (hn : 0 < n) : Tendsto (fun x : α ↦ x ^ n) atTop atTop
Full source 
lemma tendsto_zpow_atTop_atTop {n : ℤ} (hn : 0 < n) : Tendsto (fun x : α ↦ x ^ n) atTop atTop := by
  lift n to ℕ using hn.le; simp [(Int.ofNat_pos.mp hn).ne']
Power function tends to infinity at infinity for positive integer exponents
Informal description
Let $\alpha$ be a linearly ordered field. For any positive integer $n \in \mathbb{Z}_{>0}$, the function $x \mapsto x^n$ tends to $+\infty$ as $x$ tends to $+\infty$.
Filter.tendsto_const_mul_atBot_of_pos theorem
(hr : 0 < r) : Tendsto (fun x => r * f x) l atBot ↔ Tendsto f l atBot
Full source 
/-- 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 tendsto_const_mul_atBot_of_pos (hr : 0 < r) :
    TendstoTendsto (fun x => r * f x) l atBot ↔ Tendsto f l atBot := by
  simpa only [← mul_neg, ← tendsto_neg_atTop_iff] using tendsto_const_mul_atTop_of_pos hr
Multiplication by positive constant preserves divergence to $-\infty$
Informal description
Let $r$ be a positive real number and $f$ a function. Then the function $x \mapsto r \cdot f(x)$ tends to negative infinity along a filter $l$ if and only if $f$ tends to negative infinity along the same filter $l$.
Filter.tendsto_mul_const_atBot_of_pos theorem
(hr : 0 < r) : Tendsto (fun x => f x * r) l atBot ↔ Tendsto f l atBot
Full source 
/-- 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 tendsto_mul_const_atBot_of_pos (hr : 0 < r) :
    TendstoTendsto (fun x => f x * r) l atBot ↔ Tendsto f l atBot := by
  simpa only [mul_comm] using tendsto_const_mul_atBot_of_pos hr
Right multiplication by positive constant preserves divergence to $-\infty$
Informal description
Let $r$ be a positive real number and $f$ a function. Then the function $x \mapsto f(x) \cdot r$ tends to negative infinity along a filter $l$ if and only if $f$ tends to negative infinity along the same filter $l$.
Filter.tendsto_div_const_atBot_of_pos theorem
(hr : 0 < r) : Tendsto (fun x ↦ f x / r) l atBot ↔ Tendsto f l atBot
Full source 
/-- 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. -/
lemma tendsto_div_const_atBot_of_pos (hr : 0 < r) :
    TendstoTendsto (fun x ↦ f x / r) l atBot ↔ Tendsto f l atBot := by
  simp [div_eq_mul_inv, tendsto_mul_const_atBot_of_pos, hr]
Division by positive constant preserves divergence to $-\infty$
Informal description
Let $r$ be a positive real number. A function $f$ tends to negative infinity along a filter $l$ if and only if the function $x \mapsto f(x)/r$ tends to negative infinity along the same filter $l$.
Filter.tendsto_const_mul_atTop_of_neg theorem
(hr : r < 0) : Tendsto (fun x => r * f x) l atTop ↔ Tendsto f l atBot
Full source 
/-- 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 tendsto_const_mul_atTop_of_neg (hr : r < 0) :
    TendstoTendsto (fun x => r * f x) l atTop ↔ Tendsto f l atBot := by
  simpa only [neg_mul, tendsto_neg_atBot_iff] using tendsto_const_mul_atBot_of_pos (neg_pos.2 hr)
Multiplication by Negative Constant Tends to Infinity iff Function Tends to Negative Infinity
Informal description
Let $r$ be a negative real number and $f$ a function. Then the function $x \mapsto r \cdot f(x)$ tends to $+\infty$ along a filter $l$ if and only if $f$ tends to $-\infty$ along $l$.
Filter.tendsto_mul_const_atTop_of_neg theorem
(hr : r < 0) : Tendsto (fun x => f x * r) l atTop ↔ Tendsto f l atBot
Full source 
/-- 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 tendsto_mul_const_atTop_of_neg (hr : r < 0) :
    TendstoTendsto (fun x => f x * r) l atTop ↔ Tendsto f l atBot := by
  simpa only [mul_comm] using tendsto_const_mul_atTop_of_neg hr
Multiplication by Negative Constant Tends to Infinity iff Function Tends to Negative Infinity (Right Multiplication Variant)
Informal description
Let $r$ be a negative real number and $f$ a function. Then the function $x \mapsto f(x) \cdot r$ tends to $+\infty$ along a filter $l$ if and only if $f$ tends to $-\infty$ along $l$.
Filter.tendsto_div_const_atTop_of_neg theorem
(hr : r < 0) : Tendsto (fun x ↦ f x / r) l atTop ↔ Tendsto f l atBot
Full source 
/-- 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`. -/
lemma tendsto_div_const_atTop_of_neg (hr : r < 0) :
    TendstoTendsto (fun x ↦ f x / r) l atTop ↔ Tendsto f l atBot := by
  simp [div_eq_mul_inv, tendsto_mul_const_atTop_of_neg, hr]
Division by Negative Constant Tends to Infinity iff Function Tends to Negative Infinity
Informal description
Let $r$ be a negative real number and $f$ a function. Then the function $x \mapsto f(x) / r$ tends to $+\infty$ along a filter $l$ if and only if $f$ tends to $-\infty$ along $l$.
Filter.tendsto_const_mul_atBot_of_neg theorem
(hr : r < 0) : Tendsto (fun x => r * f x) l atBot ↔ Tendsto f l atTop
Full source 
/-- 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 tendsto_const_mul_atBot_of_neg (hr : r < 0) :
    TendstoTendsto (fun x => r * f x) l atBot ↔ Tendsto f l atTop := by
  simpa only [neg_mul, tendsto_neg_atTop_iff] using tendsto_const_mul_atTop_of_pos (neg_pos.2 hr)
Multiplication by Negative Constant Reverses Tendency to Infinity: $r \cdot f(x) \to -\infty \leftrightarrow f(x) \to \infty$
Informal description
Let $r$ be a negative real number and $f$ be a function. Then the function $x \mapsto r \cdot f(x)$ tends to negative infinity along a filter $l$ if and only if $f$ tends to infinity along the same filter $l$.
Filter.tendsto_mul_const_atBot_of_neg theorem
(hr : r < 0) : Tendsto (fun x => f x * r) l atBot ↔ Tendsto f l atTop
Full source 
/-- 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 tendsto_mul_const_atBot_of_neg (hr : r < 0) :
    TendstoTendsto (fun x => f x * r) l atBot ↔ Tendsto f l atTop := by
  simpa only [mul_comm] using tendsto_const_mul_atBot_of_neg hr
Multiplication by Negative Constant Reverses Tendency to Infinity: $f(x) \cdot r \to -\infty \leftrightarrow f(x) \to \infty$
Informal description
Let $r$ be a negative real number and $f$ a function. Then the function $x \mapsto f(x) \cdot r$ tends to $-\infty$ along a filter $l$ if and only if $f$ tends to $+\infty$ along $l$.
Filter.tendsto_div_const_atBot_of_neg theorem
(hr : r < 0) : Tendsto (fun x ↦ f x / r) l atBot ↔ Tendsto f l atTop
Full source 
/-- 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`. -/
lemma tendsto_div_const_atBot_of_neg (hr : r < 0) :
    TendstoTendsto (fun x ↦ f x / r) l atBot ↔ Tendsto f l atTop := by
  simp [div_eq_mul_inv, tendsto_mul_const_atBot_of_neg, hr]
Divergence to $-\infty$ under negative division: $f(x)/r \to -\infty$ iff $f(x) \to +\infty$
Informal description
Let $r$ be a negative real number and $l$ be a filter. The function $x \mapsto f(x)/r$ tends to $-\infty$ along $l$ if and only if $f$ tends to $+\infty$ along $l$.
Filter.tendsto_const_mul_atTop_iff theorem
[NeBot l] : Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
Full source 
/-- 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 tendsto_const_mul_atTop_iff [NeBot l] :
    TendstoTendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot := by
  rcases lt_trichotomy r 0 with (hr | rfl | hr)
  · simp [hr, hr.not_lt, tendsto_const_mul_atTop_of_neg]
  · simp [not_tendsto_const_atTop]
  · simp [hr, hr.not_lt, tendsto_const_mul_atTop_of_pos]
Characterization of Tendency to $+\infty$ for $r \cdot f(x)$
Informal description
Let $l$ be a nontrivial filter. The function $x \mapsto r \cdot f(x)$ tends to $+\infty$ along $l$ if and only if either: 1. $r > 0$ and $f$ tends to $+\infty$ along $l$, or 2. $r < 0$ and $f$ tends to $-\infty$ along $l$.
Filter.tendsto_mul_const_atTop_iff theorem
[NeBot l] : Tendsto (fun x => f x * r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
Full source 
/-- 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 tendsto_mul_const_atTop_iff [NeBot l] :
    TendstoTendsto (fun x => f x * r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot := by
  simp only [mul_comm _ r, tendsto_const_mul_atTop_iff]
Characterization of Tendency to $+\infty$ for $f(x) \cdot r$
Informal description
Let $l$ be a nontrivial filter. The function $x \mapsto f(x) \cdot r$ tends to $+\infty$ along $l$ if and only if either: 1. $r > 0$ and $f$ tends to $+\infty$ along $l$, or 2. $r < 0$ and $f$ tends to $-\infty$ along $l$.
Filter.tendsto_div_const_atTop_iff theorem
[NeBot l] : Tendsto (fun x ↦ f x / r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
Full source 
/-- 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. -/
lemma tendsto_div_const_atTop_iff [NeBot l] :
    TendstoTendsto (fun x ↦ f x / r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot := by
  simp [div_eq_mul_inv, tendsto_mul_const_atTop_iff]
Characterization of Tendency to $+\infty$ for $f(x)/r$
Informal description
Let $l$ be a nontrivial filter. The function $x \mapsto f(x) / r$ tends to $+\infty$ along $l$ if and only if either: 1. $r > 0$ and $f$ tends to $+\infty$ along $l$, or 2. $r < 0$ and $f$ tends to $-\infty$ along $l$.
Filter.tendsto_const_mul_atBot_iff theorem
[NeBot l] : Tendsto (fun x => r * f x) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop
Full source 
/-- 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 tendsto_const_mul_atBot_iff [NeBot l] :
    TendstoTendsto (fun x => r * f x) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop := by
  simp only [← tendsto_neg_atTop_iff, ← mul_neg, tendsto_const_mul_atTop_iff, neg_neg]
Characterization of Tendency to $-\infty$ for $r \cdot f(x)$
Informal description
Let $l$ be a nontrivial filter. The function $x \mapsto r \cdot f(x)$ tends to negative infinity along $l$ if and only if either: 1. $r > 0$ and $f$ tends to negative infinity along $l$, or 2. $r < 0$ and $f$ tends to positive infinity along $l$.
Filter.tendsto_mul_const_atBot_iff theorem
[NeBot l] : Tendsto (fun x => f x * r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop
Full source 
/-- 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 tendsto_mul_const_atBot_iff [NeBot l] :
    TendstoTendsto (fun x => f x * r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop := by
  simp only [mul_comm _ r, tendsto_const_mul_atBot_iff]
Characterization of Tendency to Negative Infinity under Multiplication by Constant
Informal description
Let $l$ be a nontrivial filter. The function $x \mapsto f(x) \cdot r$ tends to negative infinity along $l$ if and only if either: 1. $r > 0$ and $f$ tends to negative infinity along $l$, or 2. $r < 0$ and $f$ tends to positive infinity along $l$.
Filter.tendsto_div_const_atBot_iff theorem
[NeBot l] : Tendsto (fun x ↦ f x / r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop
Full source 
/-- 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. -/
lemma tendsto_div_const_atBot_iff [NeBot l] :
    TendstoTendsto (fun x ↦ f x / r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop := by
  simp [div_eq_mul_inv, tendsto_mul_const_atBot_iff]
Characterization of Tendency to Negative Infinity under Division by Constant
Informal description
Let $l$ be a nontrivial filter. The function $x \mapsto f(x) / r$ tends to negative infinity along $l$ if and only if either: 1. $r > 0$ and $f$ tends to negative infinity along $l$, or 2. $r < 0$ and $f$ tends to positive infinity along $l$.
Filter.tendsto_const_mul_atTop_iff_neg theorem
[NeBot l] (h : Tendsto f l atBot) : Tendsto (fun x => r * f x) l atTop ↔ r < 0
Full source 
/-- 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 tendsto_const_mul_atTop_iff_neg [NeBot l] (h : Tendsto f l atBot) :
    TendstoTendsto (fun x => r * f x) l atTop ↔ r < 0 := by
  simp [tendsto_const_mul_atTop_iff, h, h.not_tendsto disjoint_atBot_atTop]
Characterization of Tendency to Infinity under Negative Scaling: $r \cdot f(x) \to +\infty \leftrightarrow r < 0$ when $f \to -\infty$
Informal description
Let $l$ be a nontrivial filter and $f$ a function such that $f$ tends to negative infinity along $l$. Then the function $x \mapsto r \cdot f(x)$ tends to positive infinity along $l$ if and only if $r < 0$.
Filter.tendsto_mul_const_atTop_iff_neg theorem
[NeBot l] (h : Tendsto f l atBot) : Tendsto (fun x => f x * r) l atTop ↔ r < 0
Full source 
/-- 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 tendsto_mul_const_atTop_iff_neg [NeBot l] (h : Tendsto f l atBot) :
    TendstoTendsto (fun x => f x * r) l atTop ↔ r < 0 := by
  simp only [mul_comm _ r, tendsto_const_mul_atTop_iff_neg h]
Characterization of Tendency to Infinity under Right Multiplication by Negative Constant: $f(x) \cdot r \to +\infty \leftrightarrow r < 0$ when $f \to -\infty$
Informal description
Let $l$ be a nontrivial filter and $f$ a function such that $f$ tends to negative infinity along $l$. Then the function $x \mapsto f(x) \cdot r$ tends to positive infinity along $l$ if and only if $r < 0$.
Filter.tendsto_div_const_atTop_iff_neg theorem
[NeBot l] (h : Tendsto f l atBot) : Tendsto (fun x ↦ f x / r) l atTop ↔ r < 0
Full source 
/-- 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`. -/
lemma tendsto_div_const_atTop_iff_neg [NeBot l] (h : Tendsto f l atBot) :
    TendstoTendsto (fun x ↦ f x / r) l atTop ↔ r < 0 := by
  simp [div_eq_mul_inv, tendsto_mul_const_atTop_iff_neg h]
Divergence to $+\infty$ under Division by Negative Constant: $f(x)/r \to +\infty \leftrightarrow r < 0$ when $f \to -\infty$
Informal description
Let $l$ be a nontrivial filter and $f$ a function such that $f$ tends to negative infinity along $l$. Then the function $x \mapsto f(x) / r$ tends to positive infinity along $l$ if and only if $r < 0$.
Filter.tendsto_const_mul_atBot_iff_pos theorem
[NeBot l] (h : Tendsto f l atBot) : Tendsto (fun x => r * f x) l atBot ↔ 0 < r
Full source 
/-- 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 tendsto_const_mul_atBot_iff_pos [NeBot l] (h : Tendsto f l atBot) :
    TendstoTendsto (fun x => r * f x) l atBot ↔ 0 < r := by
  simp [tendsto_const_mul_atBot_iff, h, h.not_tendsto disjoint_atBot_atTop]
Multiplication by Positive Constant Preserves Divergence to $-\infty$
Informal description
Let $f$ be a function that tends to $-\infty$ along a nontrivial filter $l$. Then the function $x \mapsto r \cdot f(x)$ tends to $-\infty$ along $l$ if and only if $0 < r$.
Filter.tendsto_mul_const_atBot_iff_pos theorem
[NeBot l] (h : Tendsto f l atBot) : Tendsto (fun x => f x * r) l atBot ↔ 0 < r
Full source 
/-- 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 tendsto_mul_const_atBot_iff_pos [NeBot l] (h : Tendsto f l atBot) :
    TendstoTendsto (fun x => f x * r) l atBot ↔ 0 < r := by
  simp only [mul_comm _ r, tendsto_const_mul_atBot_iff_pos h]
Right Multiplication by Positive Constant Preserves Divergence to $-\infty$
Informal description
Let $f$ be a function that tends to $-\infty$ along a nontrivial filter $l$. Then the function $x \mapsto f(x) \cdot r$ tends to $-\infty$ along $l$ if and only if $0 < r$.
Filter.tendsto_div_const_atBot_iff_pos theorem
[NeBot l] (h : Tendsto f l atBot) : Tendsto (fun x ↦ f x / r) l atBot ↔ 0 < r
Full source 
/-- 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`. -/
lemma tendsto_div_const_atBot_iff_pos [NeBot l] (h : Tendsto f l atBot) :
    TendstoTendsto (fun x ↦ f x / r) l atBot ↔ 0 < r := by
  simp [div_eq_mul_inv, tendsto_mul_const_atBot_iff_pos h]
Division by Positive Constant Preserves Divergence to $-\infty$
Informal description
Let $f$ be a function that tends to $-\infty$ along a nontrivial filter $l$. Then the function $x \mapsto f(x) / r$ tends to $-\infty$ along $l$ if and only if $0 < r$.
Filter.tendsto_const_mul_atBot_iff_neg theorem
[NeBot l] (h : Tendsto f l atTop) : Tendsto (fun x => r * f x) l atBot ↔ r < 0
Full source 
/-- 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 tendsto_const_mul_atBot_iff_neg [NeBot l] (h : Tendsto f l atTop) :
    TendstoTendsto (fun x => r * f x) l atBot ↔ r < 0 := by
  simp [tendsto_const_mul_atBot_iff, h, h.not_tendsto disjoint_atTop_atBot]
Multiplication by Negative Constant Turns Infinity to Negative Infinity
Informal description
Let $l$ be a nontrivial filter and $f$ a function such that $f$ tends to infinity along $l$. Then the function $x \mapsto r \cdot f(x)$ tends to negative infinity along $l$ if and only if $r < 0$.
Filter.tendsto_mul_const_atBot_iff_neg theorem
[NeBot l] (h : Tendsto f l atTop) : Tendsto (fun x => f x * r) l atBot ↔ r < 0
Full source 
/-- 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 tendsto_mul_const_atBot_iff_neg [NeBot l] (h : Tendsto f l atTop) :
    TendstoTendsto (fun x => f x * r) l atBot ↔ r < 0 := by
  simp only [mul_comm _ r, tendsto_const_mul_atBot_iff_neg h]
Right Multiplication by Negative Constant Turns Infinity to Negative Infinity
Informal description
Let $l$ be a nontrivial filter and $f$ a function such that $f$ tends to infinity along $l$. Then the function $x \mapsto f(x) \cdot r$ tends to negative infinity along $l$ if and only if $r < 0$.
Filter.tendsto_div_const_atBot_iff_neg theorem
[NeBot l] (h : Tendsto f l atTop) : Tendsto (fun x ↦ f x / r) l atBot ↔ r < 0
Full source 
/-- If `f` tends to infinity along a nontrivial filter,
`fun x ↦ f x / r` tends to negative infinity if and only if `r < 0`. -/
lemma tendsto_div_const_atBot_iff_neg [NeBot l] (h : Tendsto f l atTop) :
    TendstoTendsto (fun x ↦ f x / r) l atBot ↔ r < 0 := by
  simp [div_eq_mul_inv, tendsto_mul_const_atBot_iff_neg h]
Division by Negative Constant Turns Infinity to Negative Infinity
Informal description
Let $l$ be a nontrivial filter and $f$ a function such that $f$ tends to infinity along $l$. Then the function $x \mapsto f(x) / r$ tends to negative infinity along $l$ if and only if $r < 0$.
Filter.Tendsto.const_mul_atTop_of_neg theorem
(hr : r < 0) (hf : Tendsto f l atTop) : Tendsto (fun x => r * f x) l atBot
Full source 
/-- 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 Tendsto.const_mul_atTop_of_neg (hr : r < 0) (hf : Tendsto f l atTop) :
    Tendsto (fun x => r * f x) l atBot :=
  (tendsto_const_mul_atBot_of_neg hr).2 hf
Negative Constant Multiplication Reverses Tendency to Infinity: $r \cdot f(x) \to -\infty$ when $f(x) \to \infty$ and $r < 0$
Informal description
Let $r$ be a negative real number and $f$ a function such that $f$ tends to infinity along a filter $l$. Then the function $x \mapsto r \cdot f(x)$ tends to negative infinity along $l$.
Filter.Tendsto.atTop_mul_const_of_neg theorem
(hr : r < 0) (hf : Tendsto f l atTop) : Tendsto (fun x => f x * r) l atBot
Full source 
/-- 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 Tendsto.atTop_mul_const_of_neg (hr : r < 0) (hf : Tendsto f l atTop) :
    Tendsto (fun x => f x * r) l atBot :=
  (tendsto_mul_const_atBot_of_neg hr).2 hf
Right Multiplication by Negative Constant Reverses Tendency to Infinity: $f(x) \cdot r \to -\infty$ when $f(x) \to +\infty$ and $r < 0$
Informal description
Let $r$ be a negative real number and $f$ a function such that $f$ tends to $+\infty$ along a filter $l$. Then the function $x \mapsto f(x) \cdot r$ tends to $-\infty$ along $l$.
Filter.Tendsto.atTop_div_const_of_neg theorem
(hr : r < 0) (hf : Tendsto f l atTop) : Tendsto (fun x ↦ f x / r) l atBot
Full source 
/-- If a function `f` tends to infinity along a filter,
then `f` divided by a negative constant tends to negative infinity. -/
lemma Tendsto.atTop_div_const_of_neg (hr : r < 0) (hf : Tendsto f l atTop) :
    Tendsto (fun x ↦ f x / r) l atBot := (tendsto_div_const_atBot_of_neg hr).2 hf
Divergence to $-\infty$ under negative division: $f(x)/r \to -\infty$ when $f(x) \to +\infty$ and $r < 0$
Informal description
Let $r$ be a negative real number and $l$ be a filter. If a function $f$ tends to $+\infty$ along $l$, then the function $x \mapsto f(x)/r$ tends to $-\infty$ along $l$.
Filter.Tendsto.const_mul_atBot theorem
(hr : 0 < r) (hf : Tendsto f l atBot) : Tendsto (fun x => r * f x) l atBot
Full source 
/-- 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 Tendsto.const_mul_atBot (hr : 0 < r) (hf : Tendsto f l atBot) :
    Tendsto (fun x => r * f x) l atBot :=
  (tendsto_const_mul_atBot_of_pos hr).2 hf
Multiplication by positive constant preserves divergence to $-\infty$
Informal description
Let $r$ be a positive real number and $f$ a function that tends to $-\infty$ along a filter $l$. Then the function $x \mapsto r \cdot f(x)$ also tends to $-\infty$ along $l$.
Filter.Tendsto.atBot_mul_const theorem
(hr : 0 < r) (hf : Tendsto f l atBot) : Tendsto (fun x => f x * r) l atBot
Full source 
/-- 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 Tendsto.atBot_mul_const (hr : 0 < r) (hf : Tendsto f l atBot) :
    Tendsto (fun x => f x * r) l atBot :=
  (tendsto_mul_const_atBot_of_pos hr).2 hf
Right multiplication by positive constant preserves divergence to $-\infty$
Informal description
Let $r$ be a positive real number and $f$ a function that tends to $-\infty$ along a filter $l$. Then the function $x \mapsto f(x) \cdot r$ also tends to $-\infty$ along $l$.
Filter.Tendsto.atBot_div_const theorem
(hr : 0 < r) (hf : Tendsto f l atBot) : Tendsto (fun x => f x / r) l atBot
Full source 
/-- If a function `f` tends to negative infinity along a filter, then `f` divided by
a positive constant also tends to negative infinity. -/
theorem Tendsto.atBot_div_const (hr : 0 < r) (hf : Tendsto f l atBot) :
    Tendsto (fun x => f x / r) l atBot := (tendsto_div_const_atBot_of_pos hr).2 hf
Division by positive constant preserves divergence to $-\infty$
Informal description
Let $r$ be a positive real number and $f$ a function such that $f$ tends to $-\infty$ along a filter $l$. Then the function $x \mapsto f(x)/r$ also tends to $-\infty$ along $l$.
Filter.Tendsto.const_mul_atBot_of_neg theorem
(hr : r < 0) (hf : Tendsto f l atBot) : Tendsto (fun x => r * f x) l atTop
Full source 
/-- 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 Tendsto.const_mul_atBot_of_neg (hr : r < 0) (hf : Tendsto f l atBot) :
    Tendsto (fun x => r * f x) l atTop :=
  (tendsto_const_mul_atTop_of_neg hr).2 hf
Negative Constant Multiplication Reverses Divergence to $-\infty$ to $+\infty$
Informal description
Let $r$ be a negative real number and $f$ a function such that $f$ tends to $-\infty$ along a filter $l$. Then the function $x \mapsto r \cdot f(x)$ tends to $+\infty$ along $l$.
Filter.Tendsto.atBot_mul_const_of_neg theorem
(hr : r < 0) (hf : Tendsto f l atBot) : Tendsto (fun x => f x * r) l atTop
Full source 
/-- 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 Tendsto.atBot_mul_const_of_neg (hr : r < 0) (hf : Tendsto f l atBot) :
    Tendsto (fun x => f x * r) l atTop :=
  (tendsto_mul_const_atTop_of_neg hr).2 hf
Right Multiplication by Negative Constant Reverses Divergence to $-\infty$ to $+\infty$
Informal description
Let $r$ be a negative real number and $f$ a function such that $f$ tends to $-\infty$ along a filter $l$. Then the function $x \mapsto f(x) \cdot r$ tends to $+\infty$ along $l$.
Filter.tendsto_neg_const_mul_pow_atTop theorem
{c : α} {n : ℕ} (hn : n ≠ 0) (hc : c < 0) : Tendsto (fun x => c * x ^ n) atTop atBot
Full source 
theorem tendsto_neg_const_mul_pow_atTop {c : α} {n : ℕ} (hn : n ≠ 0) (hc : c < 0) :
    Tendsto (fun x => c * x ^ n) atTop atBot :=
  (tendsto_pow_atTop hn).const_mul_atTop_of_neg hc
Negative Polynomial Tendency to $-\infty$: $c x^n \to -\infty$ as $x \to +\infty$ for $c < 0$ and $n \neq 0$
Informal description
Let $\alpha$ be a linearly ordered field, $c \in \alpha$ with $c < 0$, and $n \in \mathbb{N}$ with $n \neq 0$. Then the function $x \mapsto c \cdot x^n$ tends to $-\infty$ as $x$ tends to $+\infty$.
Filter.tendsto_const_mul_pow_atBot_iff theorem
{c : α} {n : ℕ} : Tendsto (fun x => c * x ^ n) atTop atBot ↔ n ≠ 0 ∧ c < 0
Full source 
theorem tendsto_const_mul_pow_atBot_iff {c : α} {n : ℕ} :
    TendstoTendsto (fun x => c * x ^ n) atTop atBot ↔ n ≠ 0 ∧ c < 0 := by
  simp only [← tendsto_neg_atTop_iff, ← neg_mul, tendsto_const_mul_pow_atTop_iff, neg_pos]
Characterization of $c x^n \to -\infty$ as $x \to +\infty$ in ordered fields
Informal description
Let $\alpha$ be a linearly ordered field, $c \in \alpha$, and $n \in \mathbb{N}$. The function $x \mapsto c x^n$ tends to $-\infty$ as $x$ tends to $+\infty$ if and only if $n \neq 0$ and $c < 0$.