tsum_geometric_of_lt_one — Mathlib

English

If r ≥ 0 and r < 1, then the sum of the geometric series equals (1 − r)^{-1}.

Русский

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

LaTeX

$$$\\\\forall r \\\\in \\\\mathbb{R}, \\\\ 0 \\\\le r \\\\wedge r < 1 \\\\Rightarrow \\sum' n, r^n = (1 - r)^{-1}.$$$

Lean4

theorem tsum_geometric_of_lt_one {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : ∑' n : ℕ, r ^ n = (1 - r)⁻¹ :=
  (hasSum_geometric_of_lt_one h₁ h₂).tsum_eq

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