tsum_geometric_add_one — Mathlib

English

Let r be a nonnegative extended real with 0 ≤ r < 1. Then the infinite sum of r^{n+1} over n ≥ 0 converges and equals r/(1−r).

Русский

Пусть r — неотрицательная конечная бесконечная величина такавая, что 0 ≤ r < 1. Тогда бесконечная сумма ∑_{n≥0} r^{n+1} сходится и равна r/(1−r).

LaTeX

$$$$\sum_{n=0}^{\infty} r^{n+1} = \frac{r}{1 - r}. $$$$

Lean4

theorem tsum_geometric_add_one (r : ℝ≥0∞) : ∑' n : ℕ, r ^ (n + 1) = r * (1 - r)⁻¹ := by
  simp only [_root_.pow_succ', ENNReal.tsum_mul_left, ENNReal.tsum_geometric]

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