English
For any natural k and any r with ∥r∥ < 1, the series ∑_{n≥0} C(n,k) r^n converges to (1 − r)^{-(k+1)}, where C(n,k) = (n+k choose k).
Русский
Для любого натурального k и r с ∥r∥ < 1 ряд ∑_{n≥0} (n+k choose k) r^n сходится и равен (1 − r)^{-(k+1)}.
LaTeX
$$$|r| < 1 \Rightarrow \sum_{n=0}^{\infty} \binom{n+k}{k} r^n = (1 - r)^{-(k+1)}$$$
Lean4
theorem hasSum_choose_mul_geometric_of_norm_lt_one' (k : ℕ) {r : R} (hr : ‖r‖ < 1) :
HasSum (fun n ↦ (n + k).choose k * r ^ n) (Ring.inverse (1 - r) ^ (k + 1)) := by
induction k with
| zero => simpa using hasSum_geom_series_inverse r hr
| succ k
ih =>
have I1 : Summable (fun (n : ℕ) ↦ ‖(n + k).choose k * r ^ n‖) :=
by
apply summable_norm_mul_geometric_of_norm_lt_one (k := k) hr
apply isBigO_iff.2 ⟨2 ^ k, ?_⟩
filter_upwards [Ioi_mem_atTop k] with n (hn : k < n)
simp only [Real.norm_eq_abs, abs_cast, cast_pow, norm_pow]
norm_cast
calc
(n + k).choose k
_ ≤ (2 * n).choose k := (choose_le_choose k (by cutsat))
_ ≤ (2 * n) ^ k := (Nat.choose_le_pow _ _)
_ = 2 ^ k * n ^ k := Nat.mul_pow 2 n k
convert
hasSum_sum_range_mul_of_summable_norm' I1 ih.summable (summable_norm_geometric_of_norm_lt_one hr)
(summable_geometric_of_norm_lt_one hr) with
n
· have :
∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ i * r ^ (n - i) =
∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ n :=
by
apply Finset.sum_congr rfl (fun i hi ↦ ?_)
simp only [Finset.mem_range] at hi
rw [mul_assoc, ← pow_add, show i + (n - i) = n by cutsat]
simp [this, ← sum_mul, ← Nat.cast_sum, sum_range_add_choose n k, add_assoc]
· rw [ih.tsum_eq, (hasSum_geom_series_inverse r hr).tsum_eq, pow_succ]
