Sum_of_Infinite_Geometric_Sequence

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

geometric-seriesproof-sketch-childproofwiki

For |r| < 1, the sum of the infinite geometric series a + ar + ar^2 + ... equals a/(1-r).

Preamble

import Mathlib.Topology.Algebra.InfiniteSum.Real
import Mathlib.Analysis.SpecificLimits.Basic
import Mathlib.Tactic

Formal statement

theorem Sum_of_Infinite_Geometric_Sequence (a r : ℝ) (hr : |r| < 1) : HasSum (fun n : ℕ => a * r ^ n) (a / (1 - r)) := by sorry