tendsto_pow_const_mul_const_pow_of_abs_lt_one

English

If |r| < 1, then n^k r^n → 0 for any natural k.

Русский

Если |r| < 1, то для любого k ∈ ℕ выполняется n^k r^n → 0.

LaTeX

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

Lean4

/-- If `|r| < 1`, then `n ^ k r ^ n` tends to zero for any natural `k`. -/
theorem tendsto_pow_const_mul_const_pow_of_abs_lt_one (k : ℕ) {r : ℝ} (hr : |r| < 1) :
    Tendsto (fun n ↦ (n : ℝ) ^ k * r ^ n : ℕ → ℝ) atTop (𝓝 0) :=
  by
  by_cases h0 : r = 0
  · exact tendsto_const_nhds.congr' (mem_atTop_sets.2 ⟨1, fun n hn ↦ by simp [zero_lt_one.trans_le hn |>.ne', h0]⟩)
  have hr' : 1 < |r|⁻¹ := (one_lt_inv₀ (abs_pos.2 h0)).2 hr
  rw [tendsto_zero_iff_norm_tendsto_zero]
  simpa [div_eq_mul_inv] using tendsto_pow_const_div_const_pow_of_one_lt k hr'

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