isLittleO_zpow_exp_pos_mul_atTop — Mathlib

English

For any integer k and a > 0, x^k = o(exp(b x)) as x → ∞.

Русский

Для любого целого k и b > 0 имеем x^k = o(exp(b x)) при x → ∞.

LaTeX

$$$$ x^k = o\bigl( e^{b x} \bigr) \quad (x \to \infty) $$$$

Lean4

/-- `x ^ k = o(exp(b * x))` as `x → ∞` for any integer `k` and positive `b`. -/
theorem isLittleO_zpow_exp_pos_mul_atTop (k : ℤ) {b : ℝ} (hb : 0 < b) :
    (fun x : ℝ => x ^ k) =o[atTop] fun x => exp (b * x) := by
  simpa only [Real.rpow_intCast] using isLittleO_rpow_exp_pos_mul_atTop k hb

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