Mathlib.Order.Filter.AtTopBot.Ring

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

theorem Tendsto.atTop_mul_atTop₀ (hf : Tendsto f l atTop) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x * g x) l atTop := by
  refine tendsto_atTop_mono' _ ?_ hg
  filter_upwards [hg.eventually (eventually_ge_atTop 0),
    hf.eventually (eventually_ge_atTop 1)] with _ using le_mul_of_one_le_left

Product of Functions Tending to Infinity Tends to Infinity

Informal description

Let $R$ be an ordered semiring and $l$ be a filter on a type $\alpha$. For functions $f, g : \alpha \to R$, if both $f$ and $g$ tend to $+\infty$ with respect to $l$, then their pointwise product $f \cdot g$ also tends to $+\infty$ with respect to $l$.

Filter.tendsto_mul_self_atTop theorem

: Tendsto (fun x : α => x * x) atTop atTop

Full source

theorem tendsto_mul_self_atTop : Tendsto (fun x : α => x * x) atTop atTop :=
  tendsto_id.atTop_mul_atTop₀ tendsto_id

Square Function Tends to Infinity at Infinity

Informal description

Let $R$ be an ordered semiring. The function $x \mapsto x^2$ tends to $+\infty$ as $x$ tends to $+\infty$ in $R$.

Filter.tendsto_pow_atTop theorem

{n : ℕ} (hn : n ≠ 0) : Tendsto (fun x : α => x ^ n) atTop atTop

Full source

/-- The monomial function `x^n` tends to `+∞` at `+∞` for any positive natural `n`.
A version for positive real powers exists as `tendsto_rpow_atTop`. -/
theorem tendsto_pow_atTop {n : ℕ} (hn : n ≠ 0) : Tendsto (fun x : α => x ^ n) atTop atTop :=
  tendsto_atTop_mono' _ ((eventually_ge_atTop 1).mono fun _x hx => le_self_pow₀ hx hn) tendsto_id

Monomial Tendency to Infinity: $x^n \to +\infty$ as $x \to +\infty$ for $n > 0$

Informal description

Let $R$ be an ordered semiring. For any positive natural number $n$, the monomial function $x \mapsto x^n$ tends to $+\infty$ as $x$ tends to $+\infty$ in $R$.

Filter.zero_pow_eventuallyEq theorem

[MonoidWithZero α] : (fun n : ℕ => (0 : α) ^ n) =ᶠ[atTop] fun _ => 0

Full source

theorem zero_pow_eventuallyEq [MonoidWithZero α] :
    (fun n : ℕ => (0 : α) ^ n) =ᶠ[atTop] fun _ => 0 :=
  eventually_atTop.2 ⟨1, fun _n hn ↦ zero_pow <| Nat.one_le_iff_ne_zero.1 hn⟩

Eventual Vanishing of Zero to the Power of $n$ in Monoids with Zero

Informal description

For any monoid with zero $\alpha$, the function $n \mapsto 0^n$ is eventually equal to the zero function in the filter `atTop` on $\mathbb{N}$. That is, there exists a natural number $N$ such that for all $n \geq N$, $0^n = 0$.

Filter.Tendsto.atTop_mul_atBot₀ theorem

(hf : Tendsto f l atTop) (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atBot

Full source

theorem Tendsto.atTop_mul_atBot₀ (hf : Tendsto f l atTop) (hg : Tendsto g l atBot) :
    Tendsto (fun x => f x * g x) l atBot := by
  have := hf.atTop_mul_atTop₀ <| tendsto_neg_atBot_atTop.comp hg
  simpa only [Function.comp_def, neg_mul_eq_mul_neg, neg_neg] using
    tendsto_neg_atTop_atBot.comp this

Product of Functions Tending to $+\infty$ and $-\infty$ Tends to $-\infty$

Informal description

Let $R$ be an ordered semiring and $l$ be a filter on a type $\alpha$. For functions $f, g : \alpha \to R$, if $f$ tends to $+\infty$ and $g$ tends to $-\infty$ with respect to $l$, then their pointwise product $f \cdot g$ tends to $-\infty$ with respect to $l$.

Filter.Tendsto.atBot_mul_atTop₀ theorem

(hf : Tendsto f l atBot) (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atBot

Full source

theorem Tendsto.atBot_mul_atTop₀ (hf : Tendsto f l atBot) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x * g x) l atBot := by
  have : Tendsto (fun x => -f x * g x) l atTop :=
    (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop₀ hg
  simpa only [Function.comp_def, neg_mul_eq_neg_mul, neg_neg] using
    tendsto_neg_atTop_atBot.comp this

Product of Functions Tending to Negative and Positive Infinity Tends to Negative Infinity

Informal description

Let $R$ be an ordered semiring and $l$ be a filter on a type $\alpha$. For functions $f, g : \alpha \to R$, if $f$ tends to $-\infty$ and $g$ tends to $+\infty$ with respect to $l$, then their pointwise product $f \cdot g$ 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 atTop

Full source

theorem Tendsto.atBot_mul_atBot₀ (hf : Tendsto f l atBot) (hg : Tendsto g l atBot) :
    Tendsto (fun x => f x * g x) l atTop := by
  have : Tendsto (fun x => -f x * -g x) l atTop :=
    (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop₀ (tendsto_neg_atBot_atTop.comp hg)
  simpa only [neg_mul_neg] using this

Product of Functions Tending to Negative Infinity Tends to Positive Infinity

Informal description

Let $R$ be an ordered semiring and $l$ be a filter on a type $\alpha$. For functions $f, g : \alpha \to R$, if both $f$ and $g$ tend to $-\infty$ with respect to $l$, then their pointwise product $f \cdot g$ tends to $+\infty$ with respect to $l$.

Filter.Tendsto.atTop_of_const_mul₀ theorem

{c : α} (hc : 0 < c) (hf : Tendsto (fun x => c * f x) l atTop) : Tendsto f l atTop

Full source

theorem Tendsto.atTop_of_const_mul₀ {c : α} (hc : 0 < c) (hf : Tendsto (fun x => c * f x) l atTop) :
    Tendsto f l atTop :=
  tendsto_atTop.2 fun b => (tendsto_atTop.1 hf (c * b)).mono
    fun _x hx => le_of_mul_le_mul_left hx hc

Tendency to Infinity under Positive Constant Multiplication

Informal description

Let $\alpha$ be a linearly ordered ring, $f : \alpha \to \alpha$ a function, and $l$ a filter on $\alpha$. For any positive constant $c > 0$ in $\alpha$, if the function $x \mapsto c \cdot f(x)$ tends to $+\infty$ with respect to $l$, then $f$ itself tends to $+\infty$ with respect to $l$.

Filter.Tendsto.atTop_of_mul_const₀ theorem

{c : α} (hc : 0 < c) (hf : Tendsto (fun x => f x * c) l atTop) : Tendsto f l atTop

Full source

theorem Tendsto.atTop_of_mul_const₀ {c : α} (hc : 0 < c) (hf : Tendsto (fun x => f x * c) l atTop) :
    Tendsto f l atTop :=
  tendsto_atTop.2 fun b => (tendsto_atTop.1 hf (b * c)).mono
    fun _x hx => le_of_mul_le_mul_right hx hc

Tendency to $+\infty$ preserved under multiplication by positive constant

Informal description

Let $f$ be a function from a type $\alpha$ to a linearly ordered ring $R$, and let $l$ be a filter on $\alpha$. If there exists a positive constant $c > 0$ in $R$ such that the function $x \mapsto f(x) \cdot c$ tends to $+\infty$ with respect to $l$, then $f$ itself tends to $+\infty$ with respect to $l$.

Filter.tendsto_pow_atTop_iff theorem

{n : ℕ} : Tendsto (fun x : α => x ^ n) atTop atTop ↔ n ≠ 0

Full source

@[simp]
theorem tendsto_pow_atTop_iff {n : ℕ} : TendstoTendsto (fun x : α => x ^ n) atTop atTop ↔ n ≠ 0 :=
  ⟨fun h hn => by simp only [hn, pow_zero, not_tendsto_const_atTop] at h, tendsto_pow_atTop⟩

Monomial Tendency to Infinity: $x^n \to +\infty$ as $x \to +\infty$ if and only if $n > 0$

Informal description

Let $R$ be a linearly ordered ring. For any natural number $n$, the monomial function $x \mapsto x^n$ tends to $+\infty$ as $x$ tends to $+\infty$ if and only if $n \neq 0$.

Filter.not_tendsto_pow_atTop_atBot theorem

[Ring α] [LinearOrder α] [IsStrictOrderedRing α] : ∀ {n : ℕ}, ¬Tendsto (fun x : α => x ^ n) atTop atBot

Full source

theorem not_tendsto_pow_atTop_atBot [Ring α] [LinearOrder α] [IsStrictOrderedRing α] :
    ∀ {n : ℕ}, ¬Tendsto (fun x : α => x ^ n) atTop atBot
  | 0 => by simp [not_tendsto_const_atBot]
  | n + 1 => (tendsto_pow_atTop n.succ_ne_zero).not_tendsto disjoint_atTop_atBot

Monomial functions do not tend to $-\infty$ at $+\infty$ in strict ordered rings

Informal description

Let $\alpha$ be a linearly ordered ring that is a strict ordered semiring. For any natural number $n$, the function $x \mapsto x^n$ does not tend to $-\infty$ as $x$ tends to $+\infty$.

exists_lt_mul_self theorem

(a : R) : ∃ x ≥ 0, a < x * x

Full source

theorem exists_lt_mul_self (a : R) : ∃ x ≥ 0, a < x * x :=
  ((eventually_ge_atTop 0).and (tendsto_mul_self_atTop.eventually (eventually_gt_atTop a))).exists

Existence of Square Dominating Element in Strict Ordered Semirings

Informal description

For any element $a$ in a strict ordered semiring $R$, there exists a non-negative element $x \in R$ such that $a < x^2$.

exists_le_mul_self theorem

(a : R) : ∃ x ≥ 0, a ≤ x * x

Full source

theorem exists_le_mul_self (a : R) : ∃ x ≥ 0, a ≤ x * x :=
  let ⟨x, hx0, hxa⟩ := exists_lt_mul_self a
  ⟨x, hx0, hxa.le⟩

Existence of Square Bounding Element in Strict Ordered Semirings

Informal description

For any element $a$ in a strict ordered semiring $R$, there exists a non-negative element $x \in R$ such that $a \leq x^2$.