doc-next-gen

Mathlib.Order.Filter.AtTopBot.Monoid

Module docstring

{"# Convergence to ±infinity in ordered commutative monoids "}

Filter.Tendsto.one_eventuallyLE_mul_atTop theorem
(hf : 1 ≤ᶠ[l] f) (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atTop
Full source 
@[to_additive]
theorem Tendsto.one_eventuallyLE_mul_atTop (hf : 1 ≤ᶠ[l] f) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x * g x) l atTop :=
  tendsto_atTop_mono' l (hf.mono fun _ ↦ le_mul_of_one_le_left') hg
Eventual Lower Bound and Tendency to Infinity Imply Product Tends to Infinity
Informal description
Let $\alpha$ be an ordered commutative monoid, and let $l$ be a filter on a type. Given functions $f, g : \alpha \to \alpha$ such that $1 \leq f(x)$ eventually with respect to $l$ and $g$ tends to $\infty$ (i.e., $\mathrm{atTop}$) with respect to $l$, then the function $x \mapsto f(x) \cdot g(x)$ also tends to $\infty$ with respect to $l$.
Filter.Tendsto.eventuallyLE_one_mul_atBot theorem
(hf : f ≤ᶠ[l] 1) (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atBot
Full source 
@[to_additive]
theorem Tendsto.eventuallyLE_one_mul_atBot (hf : f ≤ᶠ[l] 1) (hg : Tendsto g l atBot) :
    Tendsto (fun x => f x * g x) l atBot :=
  hg.one_eventuallyLE_mul_atTop (M := Mᵒᵈ) hf
Eventual Upper Bound and Tendency to Negative Infinity Imply Product Tends to Negative Infinity
Informal description
Let $\alpha$ be an ordered commutative monoid, and let $l$ be a filter on a type. Given functions $f, g : \alpha \to \alpha$ such that $f(x) \leq 1$ eventually with respect to $l$ and $g$ tends to $-\infty$ (i.e., $\mathrm{atBot}$) with respect to $l$, then the function $x \mapsto f(x) \cdot g(x)$ also tends to $-\infty$ with respect to $l$.
Filter.Tendsto.one_le_mul_atTop theorem
(hf : ∀ x, 1 ≤ f x) (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atTop
Full source 
@[to_additive]
theorem Tendsto.one_le_mul_atTop (hf : ∀ x, 1 ≤ f x) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x * g x) l atTop :=
  hg.one_eventuallyLE_mul_atTop (.of_forall hf)
Product of a Uniformly Bounded Below Function and a Function Tending to Infinity Tends to Infinity
Informal description
Let $\alpha$ be an ordered commutative monoid and $l$ a filter on a type. Given functions $f, g : \alpha \to \alpha$ such that $1 \leq f(x)$ for all $x$ and $g$ tends to $\infty$ (i.e., tends to $\mathrm{atTop}$) with respect to $l$, then the function $x \mapsto f(x) \cdot g(x)$ also tends to $\infty$ with respect to $l$.
Filter.Tendsto.le_one_mul_atBot theorem
(hf : ∀ x, f x ≤ 1) (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atBot
Full source 
@[to_additive]
theorem Tendsto.le_one_mul_atBot (hf : ∀ x, f x ≤ 1) (hg : Tendsto g l atBot) :
    Tendsto (fun x => f x * g x) l atBot :=
  hg.eventuallyLE_one_mul_atBot (.of_forall hf)
Product of a Uniformly Bounded Above Function and a Function Tending to Negative Infinity Tends to Negative Infinity
Informal description
Let $\alpha$ be an ordered commutative monoid and $l$ a filter on a type. Given functions $f, g : \alpha \to \alpha$ such that $f(x) \leq 1$ for all $x$ and $g$ tends to $-\infty$ (i.e., tends to $\mathrm{atBot}$) with respect to $l$, then the function $x \mapsto f(x) \cdot g(x)$ also tends to $-\infty$ with respect to $l$.
Filter.Tendsto.atTop_mul_one_eventuallyLE theorem
(hf : Tendsto f l atTop) (hg : 1 ≤ᶠ[l] g) : Tendsto (fun x => f x * g x) l atTop
Full source 
@[to_additive]
theorem Tendsto.atTop_mul_one_eventuallyLE (hf : Tendsto f l atTop) (hg : 1 ≤ᶠ[l] g) :
    Tendsto (fun x => f x * g x) l atTop :=
  tendsto_atTop_mono' l (hg.mono fun _ => le_mul_of_one_le_right') hf
Product of a Function Tending to Infinity and an Eventually Greater-Than-One Function Tends to Infinity
Informal description
Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder, and let $l$ be a filter on $\alpha$. Given functions $f, g : \alpha \to \beta$ such that $f$ tends to $\mathrm{atTop}$ (the filter representing the limit at positive infinity in $\beta$) with respect to $l$, and $1 \leq g(x)$ holds eventually with respect to $l$, then the function $x \mapsto f(x) \cdot g(x)$ also tends to $\mathrm{atTop}$ with respect to $l$.
Filter.Tendsto.atBot_mul_eventuallyLE_one theorem
(hf : Tendsto f l atBot) (hg : g ≤ᶠ[l] 1) : Tendsto (fun x => f x * g x) l atBot
Full source 
@[to_additive]
theorem Tendsto.atBot_mul_eventuallyLE_one (hf : Tendsto f l atBot) (hg : g ≤ᶠ[l] 1) :
    Tendsto (fun x => f x * g x) l atBot :=
  hf.atTop_mul_one_eventuallyLE (M := Mᵒᵈ) hg
Product of a Function Tending to Negative Infinity and an Eventually Less-Than-One Function Tends to Negative Infinity
Informal description
Let $f$ and $g$ be functions from a type $\alpha$ to a partially ordered commutative monoid $\beta$, and let $l$ be a filter on $\alpha$. If $f$ tends to $-\infty$ (i.e., $\mathrm{atBot}$) with respect to $l$, and $g(x) \leq 1$ holds eventually with respect to $l$, then the function $x \mapsto f(x) \cdot g(x)$ also tends to $-\infty$ with respect to $l$.
Filter.Tendsto.atTop_mul_one_le theorem
(hf : Tendsto f l atTop) (hg : ∀ x, 1 ≤ g x) : Tendsto (fun x => f x * g x) l atTop
Full source 
@[to_additive]
theorem Tendsto.atTop_mul_one_le (hf : Tendsto f l atTop) (hg : ∀ x, 1 ≤ g x) :
    Tendsto (fun x => f x * g x) l atTop :=
  hf.atTop_mul_one_eventuallyLE <| .of_forall hg
Product of a Divergent Function and a Function Bounded Below by One Diverges to Infinity
Informal description
Let $f, g : \alpha \to \beta$ be functions from a type $\alpha$ to a preordered commutative monoid $\beta$, and let $l$ be a filter on $\alpha$. If $f$ tends to $\infty$ (i.e., tends to $\mathrm{atTop}$) with respect to $l$, and $g(x) \geq 1$ for all $x \in \alpha$, then the function $x \mapsto f(x) \cdot g(x)$ also tends to $\infty$ with respect to $l$.
Filter.Tendsto.atBot_mul_le_one theorem
(hf : Tendsto f l atBot) (hg : ∀ x, g x ≤ 1) : Tendsto (fun x => f x * g x) l atBot
Full source 
@[to_additive]
theorem Tendsto.atBot_mul_le_one (hf : Tendsto f l atBot) (hg : ∀ x, g x ≤ 1) :
    Tendsto (fun x => f x * g x) l atBot :=
  hf.atBot_mul_eventuallyLE_one (.of_forall hg)
Product of a Divergent-to-Negative-Infinity Function and a Pointwise-Less-Than-One Function Diverges to Negative Infinity
Informal description
Let $f, g : \alpha \to \beta$ be functions from a type $\alpha$ to a partially ordered commutative monoid $\beta$, and let $l$ be a filter on $\alpha$. If $f$ tends to $-\infty$ (i.e., tends to $\mathrm{atBot}$) with respect to $l$, and $g(x) \leq 1$ for all $x \in \alpha$, then the function $x \mapsto f(x) \cdot g(x)$ also tends to $-\infty$ with respect to $l$.
Filter.Tendsto.atTop_mul_atTop theorem
(hf : Tendsto f l atTop) (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atTop
Full source 
/-- In an ordered multiplicative monoid, if `f` and `g` tend to `+∞`, then so does `f * g`.

Earlier, this name was used for a similar lemma about semirings,
which is now called `Filter.Tendsto.atTop_mul_atTop₀`. -/
@[to_additive]
theorem Tendsto.atTop_mul_atTop (hf : Tendsto f l atTop) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x * g x) l atTop :=
  hf.atTop_mul_one_eventuallyLE <| hg.eventually_ge_atTop 1
Product of Functions Tending to Infinity Tends to Infinity in Ordered Commutative Monoids
Informal description
Let $\alpha$ be a type with a filter $l$, and let $\beta$ be an ordered commutative monoid. Given two functions $f, g : \alpha \to \beta$ such that $f$ tends to $+\infty$ and $g$ tends to $+\infty$ with respect to $l$, then the product function $x \mapsto f(x) \cdot g(x)$ also tends to $+\infty$ with respect to $l$.
Filter.Tendsto.atBot_mul_atBot theorem
(hf : Tendsto f l atBot) (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atBot
Full source 
/-- In an ordered multiplicative monoid, if `f` and `g` tend to `-∞`, then so does `f * g`.

Earlier, this name was used for a similar lemma about rings (with conclusion `f * g → +∞`),
which is now called `Filter.Tendsto.atBot_mul_atBot₀`. -/
@[to_additive]
theorem Tendsto.atBot_mul_atBot (hf : Tendsto f l atBot) (hg : Tendsto g l atBot) :
    Tendsto (fun x => f x * g x) l atBot :=
  hf.atTop_mul_atTop (M := Mᵒᵈ) hg
Product of Functions Tending to Negative Infinity Tends to Negative Infinity in Ordered Commutative Monoids
Informal description
Let $M$ be an ordered commutative monoid, $l$ a filter on a type $\alpha$, and $f, g : \alpha \to M$ functions. If both $f$ and $g$ tend to $-\infty$ along $l$ (i.e., $\lim_{l} f = -\infty$ and $\lim_{l} g = -\infty$), then the product function $x \mapsto f(x) \cdot g(x)$ also tends to $-\infty$ along $l$.
Filter.Tendsto.atTop_pow theorem
(hf : Tendsto f l atTop) {n : ℕ} (hn : 0 < n) : Tendsto (fun x => f x ^ n) l atTop
Full source 
@[to_additive nsmul_atTop]
theorem Tendsto.atTop_pow (hf : Tendsto f l atTop) {n : ℕ} (hn : 0 < n) :
    Tendsto (fun x => f x ^ n) l atTop := by
  refine tendsto_atTop_mono' _ ((hf.eventually_ge_atTop 1).mono fun x hx ↦ ?_) hf
  simpa only [pow_one] using pow_le_pow_right' hx hn
Tendency to Infinity under Powers in Ordered Commutative Monoids
Informal description
Let $M$ be an ordered commutative monoid, $l$ a filter on a type $\alpha$, and $f : \alpha \to M$ a function. If $f$ tends to $+\infty$ along $l$ (i.e., $\lim_{l} f = +\infty$) and $n$ is a positive natural number, then the function $x \mapsto f(x)^n$ also tends to $+\infty$ along $l$.
Filter.Tendsto.atBot_pow theorem
(hf : Tendsto f l atBot) {n : ℕ} (hn : 0 < n) : Tendsto (fun x => f x ^ n) l atBot
Full source 
@[to_additive nsmul_atBot]
theorem Tendsto.atBot_pow (hf : Tendsto f l atBot) {n : ℕ} (hn : 0 < n) :
    Tendsto (fun x => f x ^ n) l atBot :=
  Tendsto.atTop_pow (M := Mᵒᵈ) hf hn
Tendency to Negative Infinity under Powers in Ordered Commutative Monoids
Informal description
Let $M$ be an ordered commutative monoid, $l$ a filter on a type $\alpha$, and $f : \alpha \to M$ a function. If $f$ tends to $-\infty$ along $l$ (i.e., $\lim_{l} f = -\infty$) and $n$ is a positive natural number, then the function $x \mapsto f(x)^n$ also tends to $-\infty$ along $l$.
Filter.Tendsto.atTop_of_const_mul theorem
(C : M) (hf : Tendsto (C * f ·) l atTop) : Tendsto f l atTop
Full source 
/-- In an ordered cancellative multiplicative monoid, if `C * f x → +∞`, then `f x → +∞`.

Earlier, this name was used for a similar lemma about ordered rings,
which is now called `Filter.Tendsto.atTop_of_const_mul₀`. -/
@[to_additive]
theorem Tendsto.atTop_of_const_mul (C : M) (hf : Tendsto (C * f ·) l atTop) : Tendsto f l atTop :=
  tendsto_atTop.2 fun b ↦ (tendsto_atTop.1 hf (C * b)).mono fun _ ↦ le_of_mul_le_mul_left'
Tendency to Infinity via Constant Multiplication in Ordered Cancellative Monoids
Informal description
Let $M$ be an ordered cancellative commutative monoid, $C$ an element of $M$, and $f : \alpha \to M$ a function. If the function $x \mapsto C \cdot f(x)$ tends to $+\infty$ (i.e., tends to the filter `atTop`) along a filter $l$, then $f$ itself tends to $+\infty$ along $l$.
Filter.Tendsto.atBot_of_const_mul theorem
(C : M) (hf : Tendsto (C * f ·) l atBot) : Tendsto f l atBot
Full source 
@[to_additive]
theorem Tendsto.atBot_of_const_mul (C : M) (hf : Tendsto (C * f ·) l atBot) : Tendsto f l atBot :=
  hf.atTop_of_const_mul (M := Mᵒᵈ)
Tendency to Negative Infinity via Constant Multiplication in Ordered Cancellative Monoids
Informal description
Let $M$ be an ordered cancellative commutative monoid, $C$ an element of $M$, and $f : \alpha \to M$ a function. If the function $x \mapsto C \cdot f(x)$ tends to $-\infty$ (i.e., tends to the filter `atBot`) along a filter $l$, then $f$ itself tends to $-\infty$ along $l$.
Filter.Tendsto.atTop_of_mul_const theorem
(C : M) (hf : Tendsto (f · * C) l atTop) : Tendsto f l atTop
Full source 
/-- In an ordered cancellative multiplicative monoid, if `f x * C → +∞`, then `f x → +∞`.

Earlier, this name was used for a similar lemma about ordered rings,
which is now called `Filter.Tendsto.atTop_of_mul_const₀`. -/
@[to_additive]
theorem Tendsto.atTop_of_mul_const (C : M) (hf : Tendsto (f · * C) l atTop) : Tendsto f l atTop :=
  tendsto_atTop.2 fun b => (tendsto_atTop.1 hf (b * C)).mono fun _ => le_of_mul_le_mul_right'
Tendency to Infinity via Right Multiplication in Ordered Cancellative Monoids
Informal description
Let $M$ be an ordered cancellative commutative monoid, and let $f$ be a function from some type to $M$. If for some constant $C \in M$, the product $f(x) \cdot C$ tends to $+\infty$ (i.e., for any upper bound $b \in M$, $f(x) \cdot C$ is eventually greater than $b$), then $f(x)$ itself tends to $+\infty$.
Filter.Tendsto.atBot_of_mul_const theorem
(C : M) (hf : Tendsto (f · * C) l atBot) : Tendsto f l atBot
Full source 
@[to_additive]
theorem Tendsto.atBot_of_mul_const (C : M) (hf : Tendsto (f · * C) l atBot) : Tendsto f l atBot :=
  hf.atTop_of_mul_const (M := Mᵒᵈ)
Tendency to Negative Infinity via Right Multiplication in Ordered Cancellative Monoids
Informal description
Let $M$ be an ordered cancellative commutative monoid, and let $f$ be a function from some type to $M$. If for some constant $C \in M$, the product $f(x) \cdot C$ tends to $-\infty$ (i.e., for any lower bound $b \in M$, $f(x) \cdot C$ is eventually less than $b$), then $f(x)$ itself tends to $-\infty$.
Filter.Tendsto.atTop_of_isBoundedUnder_le_mul theorem
(hf : IsBoundedUnder (· ≤ ·) l f) (hfg : Tendsto (fun x => f x * g x) l atTop) : Tendsto g l atTop
Full source 
/-- If `f` is eventually bounded from above along `l` and `f * g` tends to `+∞`,
then `g` tends to `+∞`. -/
@[to_additive "If `f` is eventually bounded from above along `l` and `f + g` tends to `+∞`,
then `g` tends to `+∞`."]
theorem Tendsto.atTop_of_isBoundedUnder_le_mul (hf : IsBoundedUnder (· ≤ ·) l f)
    (hfg : Tendsto (fun x => f x * g x) l atTop) : Tendsto g l atTop := by
  obtain ⟨C, hC⟩ := hf
  refine .atTop_of_const_mul C <| tendsto_atTop_mono' l ?_ hfg
  exact (eventually_map.mp hC).mono fun _ ↦ (mul_le_mul_right' · _)
Tendency to Infinity via Bounded Multiplicative Factor in Ordered Cancellative Monoids
Informal description
Let $M$ be an ordered cancellative commutative monoid, and let $f, g$ be functions from a type $\alpha$ to $M$. If $f$ is eventually bounded from above along a filter $l$ (i.e., there exists an upper bound $C \in M$ such that $f(x) \leq C$ for all $x$ in a set belonging to $l$), and the product $f(x) \cdot g(x)$ tends to $+\infty$ along $l$, then $g(x)$ tends to $+\infty$ along $l$.
Filter.Tendsto.atBot_of_isBoundedUnder_ge_mul theorem
(hf : IsBoundedUnder (· ≥ ·) l f) (h : Tendsto (fun x => f x * g x) l atBot) : Tendsto g l atBot
Full source 
@[to_additive]
theorem Tendsto.atBot_of_isBoundedUnder_ge_mul (hf : IsBoundedUnder (· ≥ ·) l f)
    (h : Tendsto (fun x => f x * g x) l atBot) : Tendsto g l atBot :=
  h.atTop_of_isBoundedUnder_le_mul (M := Mᵒᵈ) hf
Tendency to Negative Infinity via Bounded Multiplicative Factor in Ordered Cancellative Monoids
Informal description
Let $M$ be an ordered cancellative commutative monoid, and let $f, g$ be functions from a type $\alpha$ to $M$. If $f$ is eventually bounded from below along a filter $l$ (i.e., there exists a lower bound $C \in M$ such that $f(x) \geq C$ for all $x$ in a set belonging to $l$), and the product $f(x) \cdot g(x)$ tends to $-\infty$ along $l$, then $g(x)$ tends to $-\infty$ along $l$.
Filter.Tendsto.atTop_of_le_const_mul theorem
(hf : ∃ C, ∀ x, f x ≤ C) (hfg : Tendsto (fun x ↦ f x * g x) l atTop) : Tendsto g l atTop
Full source 
@[to_additive]
theorem Tendsto.atTop_of_le_const_mul (hf : ∃ C, ∀ x, f x ≤ C)
    (hfg : Tendsto (fun x ↦ f x * g x) l atTop) : Tendsto g l atTop :=
  hfg.atTop_of_isBoundedUnder_le_mul <| hf.imp fun _C hC ↦ eventually_map.mpr <| .of_forall hC
Tendency to Infinity via Bounded Multiplicative Factor in Ordered Cancellative Monoids
Informal description
Let $M$ be an ordered cancellative commutative monoid, and let $f, g$ be functions from a type $\alpha$ to $M$. If there exists a constant $C \in M$ such that $f(x) \leq C$ for all $x \in \alpha$, and the product $f(x) \cdot g(x)$ tends to $+\infty$ along a filter $l$, then $g(x)$ tends to $+\infty$ along $l$.
Filter.Tendsto.atBot_of_const_le_mul theorem
(hf : ∃ C, ∀ x, C ≤ f x) (hfg : Tendsto (fun x ↦ f x * g x) l atBot) : Tendsto g l atBot
Full source 
@[to_additive]
theorem Tendsto.atBot_of_const_le_mul (hf : ∃ C, ∀ x, C ≤ f x)
    (hfg : Tendsto (fun x ↦ f x * g x) l atBot) : Tendsto g l atBot :=
  Tendsto.atTop_of_le_const_mul (M := Mᵒᵈ) hf hfg
Tendency to $-\infty$ via lower bounded multiplicative factor in ordered cancellative monoids
Informal description
Let $M$ be an ordered cancellative commutative monoid, and let $f, g : \alpha \to M$ be functions. If there exists a constant $C \in M$ such that $C \leq f(x)$ for all $x \in \alpha$, and the product $f(x) \cdot g(x)$ tends to $-\infty$ along a filter $l$, then $g(x)$ tends to $-\infty$ along $l$.
Filter.Tendsto.atTop_of_mul_isBoundedUnder_le theorem
(hg : IsBoundedUnder (· ≤ ·) l g) (h : Tendsto (fun x => f x * g x) l atTop) : Tendsto f l atTop
Full source 
@[to_additive]
theorem Tendsto.atTop_of_mul_isBoundedUnder_le (hg : IsBoundedUnder (· ≤ ·) l g)
    (h : Tendsto (fun x => f x * g x) l atTop) : Tendsto f l atTop := by
  obtain ⟨C, hC⟩ := hg
  refine .atTop_of_mul_const C <| tendsto_atTop_mono' l ?_ h
  exact (eventually_map.mp hC).mono fun _ ↦ (mul_le_mul_left' · _)
Tendency to Infinity via Bounded Multiplicative Factor in Ordered Cancellative Monoids
Informal description
Let $M$ be an ordered cancellative commutative monoid, and let $f, g$ be functions from some type to $M$. If $g$ is bounded above under the order relation $\leq$ with respect to a filter $l$, and the product $f(x) \cdot g(x)$ tends to $+\infty$ with respect to $l$, then $f(x)$ itself tends to $+\infty$ with respect to $l$.
Filter.Tendsto.atBot_of_mul_isBoundedUnder_ge theorem
(hg : IsBoundedUnder (· ≥ ·) l g) (h : Tendsto (fun x => f x * g x) l atBot) : Tendsto f l atBot
Full source 
@[to_additive]
theorem Tendsto.atBot_of_mul_isBoundedUnder_ge (hg : IsBoundedUnder (· ≥ ·) l g)
    (h : Tendsto (fun x => f x * g x) l atBot) : Tendsto f l atBot :=
  h.atTop_of_mul_isBoundedUnder_le (M := Mᵒᵈ) hg
Tendency to Negative Infinity via Bounded Multiplicative Factor in Ordered Cancellative Monoids
Informal description
Let $M$ be an ordered cancellative commutative monoid, and let $f, g$ be functions from some type to $M$. If $g$ is bounded below under the order relation $\geq$ with respect to a filter $l$, and the product $f(x) \cdot g(x)$ tends to $-\infty$ with respect to $l$, then $f(x)$ itself tends to $-\infty$ with respect to $l$.
Filter.Tendsto.atTop_of_mul_le_const theorem
(hg : ∃ C, ∀ x, g x ≤ C) (hfg : Tendsto (fun x ↦ f x * g x) l atTop) : Tendsto f l atTop
Full source 
@[to_additive]
theorem Tendsto.atTop_of_mul_le_const (hg : ∃ C, ∀ x, g x ≤ C)
    (hfg : Tendsto (fun x ↦ f x * g x) l atTop) : Tendsto f l atTop :=
  hfg.atTop_of_mul_isBoundedUnder_le <| hg.imp fun _C hC ↦ eventually_map.mpr <| .of_forall hC
Tendency to Infinity via Bounded Multiplicative Factor in Ordered Cancellative Monoids
Informal description
Let $M$ be an ordered cancellative commutative monoid, and let $f, g$ be functions from some type to $M$. If there exists a constant $C$ such that $g(x) \leq C$ for all $x$, and the product $f(x) \cdot g(x)$ tends to $+\infty$ with respect to a filter $l$, then $f(x)$ itself tends to $+\infty$ with respect to $l$.
Filter.Tendsto.atBot_of_mul_const_le theorem
(hg : ∃ C, ∀ x, C ≤ g x) (hfg : Tendsto (fun x ↦ f x * g x) l atBot) : Tendsto f l atBot
Full source 
@[to_additive]
theorem Tendsto.atBot_of_mul_const_le (hg : ∃ C, ∀ x, C ≤ g x)
    (hfg : Tendsto (fun x ↦ f x * g x) l atBot) : Tendsto f l atBot :=
  Tendsto.atTop_of_mul_le_const (M := Mᵒᵈ) hg hfg
Tendency to Negative Infinity via Bounded Below Multiplicative Factor in Ordered Cancellative Monoids
Informal description
Let $M$ be an ordered cancellative commutative monoid, and let $f, g$ be functions from some type to $M$. If there exists a constant $C$ such that $C \leq g(x)$ for all $x$, and the product $f(x) \cdot g(x)$ tends to $-\infty$ with respect to a filter $l$, then $f(x)$ itself tends to $-\infty$ with respect to $l$.
Filter.tendsto_atTop_of_add_bdd_above_left' theorem
(C) (hC : ∀ᶠ x in l, f x ≤ C) (h : Tendsto (fun x => f x + g x) l atTop) : Tendsto g l atTop
Full source 
@[deprecated Tendsto.atTop_of_isBoundedUnder_le_add (since := "2025-02-13")]
theorem tendsto_atTop_of_add_bdd_above_left' (C) (hC : ∀ᶠ x in l, f x ≤ C)
    (h : Tendsto (fun x => f x + g x) l atTop) : Tendsto g l atTop :=
  .atTop_of_isBoundedUnder_le_add ⟨C, hC⟩ h
Tendency to $+\infty$ of a function with bounded additive perturbation
Informal description
Let $f$ and $g$ be functions defined on a type with a preorder, and let $l$ be a filter. If there exists a constant $C$ such that $f(x) \leq C$ for all $x$ in the filter $l$, and the sum $f(x) + g(x)$ tends to $+\infty$ along $l$, then $g(x)$ tends to $+\infty$ along $l$.
Filter.tendsto_atBot_of_add_bdd_below_left' theorem
(C) (hC : ∀ᶠ x in l, C ≤ f x) (h : Tendsto (fun x => f x + g x) l atBot) : Tendsto g l atBot
Full source 
@[deprecated Tendsto.atBot_of_isBoundedUnder_ge_add (since := "2025-02-13")]
theorem tendsto_atBot_of_add_bdd_below_left' (C) (hC : ∀ᶠ x in l, C ≤ f x)
    (h : Tendsto (fun x => f x + g x) l atBot) : Tendsto g l atBot :=
  .atBot_of_isBoundedUnder_ge_add ⟨C, hC⟩ h
Tendency to $-\infty$ of a function with bounded below additive perturbation
Informal description
Let $f$ and $g$ be functions from a type to an ordered cancellative additive commutative monoid $\alpha$, and let $l$ be a filter. If there exists a constant $C$ such that $C \leq f(x)$ for all $x$ in the filter $l$, and the sum $f(x) + g(x)$ tends to $-\infty$ along $l$, then $g(x)$ tends to $-\infty$ along $l$.
Filter.tendsto_atTop_of_add_bdd_above_left theorem
(C) (hC : ∀ x, f x ≤ C) : Tendsto (fun x => f x + g x) l atTop → Tendsto g l atTop
Full source 
@[deprecated Tendsto.atTop_of_le_const_add (since := "2025-02-13")]
theorem tendsto_atTop_of_add_bdd_above_left (C) (hC : ∀ x, f x ≤ C) :
    Tendsto (fun x => f x + g x) l atTop → Tendsto g l atTop :=
  .atTop_of_le_const_add ⟨C, hC⟩
Tendency to $+\infty$ for a function when its sum with a bounded-above function tends to $+\infty$ (uniform version)
Informal description
Let $\alpha$ be an ordered cancellative additive monoid, and let $f$ and $g$ be functions defined on a filter $l$ with values in $\alpha$. If there exists a constant $C$ such that $f(x) \leq C$ for all $x$, and the sum $f(x) + g(x)$ tends to $+\infty$ along $l$, then $g(x)$ tends to $+\infty$ along $l$.
Filter.tendsto_atBot_of_add_bdd_below_left theorem
(C) (hC : ∀ x, C ≤ f x) : Tendsto (fun x => f x + g x) l atBot → Tendsto g l atBot
Full source 
@[deprecated Tendsto.atBot_of_const_le_add (since := "2025-02-13")]
theorem tendsto_atBot_of_add_bdd_below_left (C) (hC : ∀ x, C ≤ f x) :
    Tendsto (fun x => f x + g x) l atBot → Tendsto g l atBot :=
  .atBot_of_const_le_add ⟨C, hC⟩
Tendency to $-\infty$ of a function with uniformly bounded below additive perturbation
Informal description
Let $\alpha$ be an ordered cancellative additive monoid, and let $f, g$ be functions defined on a filter $l$ with values in $\alpha$. If there exists a constant $C$ such that $C \leq f(x)$ for all $x$, and the sum $f(x) + g(x)$ tends to $-\infty$ along $l$, then $g(x)$ tends to $-\infty$ along $l$.
Filter.tendsto_atTop_of_add_bdd_above_right' theorem
(C) (hC : ∀ᶠ x in l, g x ≤ C) (h : Tendsto (fun x => f x + g x) l atTop) : Tendsto f l atTop
Full source 
@[deprecated Tendsto.atTop_of_add_isBoundedUnder_le (since := "2025-02-13")]
theorem tendsto_atTop_of_add_bdd_above_right' (C) (hC : ∀ᶠ x in l, g x ≤ C)
    (h : Tendsto (fun x => f x + g x) l atTop) : Tendsto f l atTop :=
  h.atTop_of_add_isBoundedUnder_le ⟨C, hC⟩
Tendency to $+\infty$ for a function when its sum with a bounded-above function tends to $+\infty$
Informal description
Let $f$ and $g$ be functions defined on a filter $l$ with values in an ordered cancellative additive monoid $\alpha$. If there exists a constant $C$ such that $g(x) \leq C$ for all $x$ in a set that is eventually in $l$, and the sum $f(x) + g(x)$ tends to $+\infty$ in $l$, then $f(x)$ tends to $+\infty$ in $l$.
Filter.tendsto_atBot_of_add_bdd_below_right' theorem
(C) (hC : ∀ᶠ x in l, C ≤ g x) (h : Tendsto (fun x => f x + g x) l atBot) : Tendsto f l atBot
Full source 
@[deprecated Tendsto.atBot_of_add_isBoundedUnder_ge (since := "2025-02-13")]
theorem tendsto_atBot_of_add_bdd_below_right' (C) (hC : ∀ᶠ x in l, C ≤ g x)
    (h : Tendsto (fun x => f x + g x) l atBot) : Tendsto f l atBot :=
  h.atBot_of_add_isBoundedUnder_ge ⟨C, hC⟩
Tendency to $-\infty$ for a function when its sum with a bounded-below function tends to $-\infty$
Informal description
Let $\alpha$ be an ordered cancellative additive monoid, and let $f, g$ be functions defined on a filter $l$ with values in $\alpha$. If there exists a constant $C$ such that $C \leq g(x)$ for all $x$ in a set that is eventually in $l$, and the sum $f(x) + g(x)$ tends to $-\infty$ in $l$, then $f(x)$ tends to $-\infty$ in $l$.
Filter.tendsto_atTop_of_add_bdd_above_right theorem
(C) (hC : ∀ x, g x ≤ C) : Tendsto (fun x => f x + g x) l atTop → Tendsto f l atTop
Full source 
@[deprecated Tendsto.atTop_of_add_le_const (since := "2025-02-13")]
theorem tendsto_atTop_of_add_bdd_above_right (C) (hC : ∀ x, g x ≤ C) :
    Tendsto (fun x => f x + g x) l atTop → Tendsto f l atTop :=
  .atTop_of_add_le_const ⟨C, hC⟩
Tendency to $+\infty$ for a function when its sum with a bounded-above function tends to $+\infty$
Informal description
Let $\alpha$ be an ordered cancellative additive monoid, and let $f, g$ be functions defined on a filter $l$ with values in $\alpha$. If there exists a constant $C$ such that $g(x) \leq C$ for all $x$, and the sum $f(x) + g(x)$ tends to $+\infty$ in $l$, then $f(x)$ tends to $+\infty$ in $l$.
Filter.tendsto_atBot_of_add_bdd_below_right theorem
(C) (hC : ∀ x, C ≤ g x) : Tendsto (fun x => f x + g x) l atBot → Tendsto f l atBot
Full source 
@[deprecated Tendsto.atBot_of_add_const_le (since := "2025-02-13")]
theorem tendsto_atBot_of_add_bdd_below_right (C) (hC : ∀ x, C ≤ g x) :
    Tendsto (fun x => f x + g x) l atBot → Tendsto f l atBot :=
  .atBot_of_add_const_le ⟨C, hC⟩
Tendency to $-\infty$ for a function when its sum with a uniformly bounded-below function tends to $-\infty$
Informal description
Let $\alpha$ be an ordered cancellative additive monoid, and let $f, g : \beta \to \alpha$ be functions. If there exists a constant $C \in \alpha$ such that $C \leq g(x)$ for all $x \in \beta$, and the function $x \mapsto f(x) + g(x)$ tends to $-\infty$ in the filter $l$, then $f$ tends to $-\infty$ in $l$.