tsum_choose_mul_geometric_of_norm_lt_one'

English

For any k and r with ∥r∥ < 1, the series ∑_{n} (n+k choose k) r^n converges to (1 − r)^{-(k+1)} in any normed ring, as a corollary of the previous results.

Русский

Для любого k и r с ∥r∥ < 1 ряд ∑_{n} (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 tsum_choose_mul_geometric_of_norm_lt_one' (k : ℕ) {r : R} (hr : ‖r‖ < 1) :
    ∑' n, (n + k).choose k * r ^ n = (Ring.inverse (1 - r)) ^ (k + 1) :=
  (hasSum_choose_mul_geometric_of_norm_lt_one' k hr).tsum_eq

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