tendsto_pow_const_div_const_pow_of_one_lt

English

For any natural k and real r > 1, (n^k)/(r^n) tends to 0 as n → ∞.

Русский

Для любого k ∈ ℕ и r > 1, (n^k)/(r^n) стремится к 0 при n → ∞.

LaTeX

$$$\\\\forall k \\\\in \\\\mathbb{N}, {r>1} \\\\Rightarrow \\\\lim_{n \\to \\infty} \\\\frac{n^k}{r^n} = 0$$$

Lean4

theorem tendsto_pow_const_div_const_pow_of_one_lt (k : ℕ) {r : ℝ} (hr : 1 < r) :
    Tendsto (fun n ↦ (n : ℝ) ^ k / r ^ n : ℕ → ℝ) atTop (𝓝 0) :=
  (isLittleO_pow_const_const_pow_of_one_lt k hr).tendsto_div_nhds_zero

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