tendsto_self_mul_const_pow_of_lt_one

English

If 0 ≤ r < 1, then n r^n → 0 for all natural n.

Русский

Если 0 ≤ r < 1, то n r^n → 0 для всех натуральных n.

LaTeX

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

Lean4

/-- If `0 ≤ r < 1`, then `n * r ^ n` tends to zero. This is a specialized version of
`tendsto_self_mul_const_pow_of_abs_lt_one`, singled out for ease of application. -/
theorem tendsto_self_mul_const_pow_of_lt_one {r : ℝ} (hr : 0 ≤ r) (h'r : r < 1) :
    Tendsto (fun n ↦ n * r ^ n : ℕ → ℝ) atTop (𝓝 0) := by
  simpa only [pow_one] using tendsto_pow_const_mul_const_pow_of_lt_one 1 hr h'r

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