isLittleO_pow_exp_pos_mul_atTop — Mathlib

English

If k ∈ ℕ and b > 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), \ k\in\mathbb{N}, b>0 $$$$

Lean4

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

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