tsum_geometric_nnreal — Mathlib

English

If r < 1, then the geometric series in NNReal is summable and its sum equals (1 − r)^{-1}.

Русский

Если r < 1, геометрическая серия в NNReal суммируема и сумма равна (1 − r)^{-1}.

LaTeX

$$$\\\\forall r \\\\in \\\\mathbb{NNReal}, \\\\ r < 1 \\\\Rightarrow \\\\ sum r^n = (1 - r)^{-1}.$$$

Lean4

theorem tsum_geometric_nnreal {r : ℝ≥0} (hr : r < 1) : ∑' n : ℕ, r ^ n = (1 - r)⁻¹ :=
  (NNReal.hasSum_geometric hr).tsum_eq

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