English
For any k ∈ ℕ and r with ∥r∥ < 1, the sum ∑_{n≥0} binom(n+k,k) r^n converges to (1−r)^{-(k+1)}.
Русский
Для любого k ∈ ℕ и r с ∥r∥ < 1 сумма ∑_{n≥0} binom(n+k,k) r^n сходится к (1−r)^{-(k+1)}.
LaTeX
$$$|r| < 1 \Rightarrow \sum_{n=0}^{\infty} {n+k \choose k} r^{n} = (1 - r)^{-(k+1)}$$$
Lean4
/-- If `‖r‖ < 1`, then `∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2`, `HasSum` version in a general ring
with summable geometric series. For a version in a field, using division instead of `Ring.inverse`,
see `hasSum_coe_mul_geometric_of_norm_lt_one`. -/
theorem hasSum_coe_mul_geometric_of_norm_lt_one' {x : R} (h : ‖x‖ < 1) :
HasSum (fun n ↦ n * x ^ n : ℕ → R) (x * (Ring.inverse (1 - x)) ^ 2) :=
by
have A : HasSum (fun (n : ℕ) ↦ (n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2) :=
by
convert hasSum_choose_mul_geometric_of_norm_lt_one' 1 h with n
simp
have B : HasSum (fun (n : ℕ) ↦ x ^ n) (Ring.inverse (1 - x)) := hasSum_geom_series_inverse x h
convert A.sub B using 1
· ext n
simp [add_mul]
· symm
calc
Ring.inverse (1 - x) ^ 2 - Ring.inverse (1 - x)
_ = Ring.inverse (1 - x) ^ 2 - ((1 - x) * Ring.inverse (1 - x)) * Ring.inverse (1 - x) := by
simp [Ring.mul_inverse_cancel (1 - x) (isUnit_one_sub_of_norm_lt_one h)]
_ = x * Ring.inverse (1 - x) ^ 2 := by noncomm_ring
