tsum_geometric_of_abs_lt_one — Mathlib

English

For a real number r with |r| < 1, the geometric series converges and its sum is (1 − r)^{-1}.

Русский

Для вещественного числа r с |r| < 1 геометрическая серия сходится и сумма равна (1 − r)^{-1}.

LaTeX

$$$|r| < 1 \Rightarrow \sum_{n=0}^{\infty} r^{n} = (1 - r)^{-1}$$$

Lean4

theorem tsum_geometric_of_abs_lt_one {r : ℝ} (h : |r| < 1) : ∑' n : ℕ, r ^ n = (1 - r)⁻¹ :=
  tsum_geometric_of_norm_lt_one h

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