isLittleO_pow_pow_atTop_of_lt — Mathlib

English

If p < q then x^p = o(x^q) as x → ∞; i.e., x^p grows strictly slower than x^q.

Русский

Если p < q, то x^p = o(x^q) при x → ∞; т. е. x^p растёт медленнее, чем x^q.

LaTeX

$$$x^p = o_{atTop} x^q \quad (p

Lean4

theorem isLittleO_pow_pow_atTop_of_lt [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [OrderTopology 𝕜] {p q : ℕ}
    (hpq : p < q) : (fun x : 𝕜 => x ^ p) =o[atTop] fun x => x ^ q :=
  by
  refine (isLittleO_iff_tendsto' ?_).mpr (tendsto_pow_div_pow_atTop_zero hpq)
  exact (eventually_gt_atTop 0).mono fun x hx hxq => (pow_ne_zero q hx.ne' hxq).elim

Похожие утверждения