tendsto_pow_const_mul_const_pow_of_lt_one

English

More generally, for any r and k ≠ 0, r/n^k → 0 as n → ∞.

Русский

Более общо, для любого r и k ≠ 0, r/n^k → 0 при n → ∞.

LaTeX

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

Lean4

/-- If `0 ≤ r < 1`, then `n ^ k r ^ n` tends to zero for any natural `k`.
This is a specialized version of `tendsto_pow_const_mul_const_pow_of_abs_lt_one`, singled out
for ease of application. -/
theorem tendsto_pow_const_mul_const_pow_of_lt_one (k : ℕ) {r : ℝ} (hr : 0 ≤ r) (h'r : r < 1) :
    Tendsto (fun n ↦ (n : ℝ) ^ k * r ^ n : ℕ → ℝ) atTop (𝓝 0) :=
  tendsto_pow_const_mul_const_pow_of_abs_lt_one k (abs_lt.2 ⟨neg_one_lt_zero.trans_le hr, h'r⟩)

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