tendsto_self_mul_const_pow_of_abs_lt_one

English

If |r| < 1, then n r^n → 0 as n → ∞.

Русский

Если |r| < 1, то n r^n → 0 при n → ∞.

LaTeX

$$$\\\\forall r \\\\in \\\\mathbb{R}, \\\\big|r\\\\big| < 1 \\\\Rightarrow \\\\lim_{n \\to \\infty} n r^n = 0$$$

Lean4

/-- If `|r| < 1`, then `n * r ^ n` tends to zero. -/
theorem tendsto_self_mul_const_pow_of_abs_lt_one {r : ℝ} (hr : |r| < 1) :
    Tendsto (fun n ↦ n * r ^ n : ℕ → ℝ) atTop (𝓝 0) := by
  simpa only [pow_one] using tendsto_pow_const_mul_const_pow_of_abs_lt_one 1 hr

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