summable_choose_mul_geometric_of_norm_lt_one

English

For any natural k and any r with ∥r∥ < 1, the sum ∑_{n≥0} (n+k choose k) r^n equals (1 − r)^{-(k+1)}.

Русский

Для любого k и r с ∥r∥ < 1 сумма ∑_{n≥0} (n+k choose 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

theorem summable_choose_mul_geometric_of_norm_lt_one (k : ℕ) {r : R} (hr : ‖r‖ < 1) :
    Summable (fun n ↦ (n + k).choose k * r ^ n) :=
  (hasSum_choose_mul_geometric_of_norm_lt_one' k hr).summable

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