English
If r with ∥r∥ < 1 and a sequence u(n) grows at most polynomially, then ∑ ∥u(n) r^n∥ converges; in particular, with u(n) = n^k, ∑ ∥n^k r^n∥ converges.
Русский
Если ∥r∥ < 1 и последовательность u(n) растет не быстрее полиномиального, то ∑ ∥u(n) r^n∥ сходится; в частности, при u(n) = n^k, ∑ ∥n^k r^n∥ сходится.
LaTeX
$$If (fun n => (n^k : ℝ)) =O[atTop] (fun n => ↑(n^k)) and ∥r∥ < 1, then Summable (fun n => ‖n^k r^n‖)$$
Lean4
/-- If `‖r‖ < 1`, then `∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2`, version in a general ring with
summable geometric series. For a version in a field, using division instead of `Ring.inverse`,
see `tsum_coe_mul_geometric_of_norm_lt_one`. -/
theorem tsum_coe_mul_geometric_of_norm_lt_one' {r : 𝕜} (hr : ‖r‖ < 1) :
(∑' n : ℕ, n * r ^ n : 𝕜) = r * Ring.inverse (1 - r) ^ 2 :=
(hasSum_coe_mul_geometric_of_norm_lt_one' hr).tsum_eq
