lean_workbook_plus_82150

Proved

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

proofwiki

Since $0 < x < 1$ , we get: $\sum_{k=0}^{+\infty}x^{2^{n+1} \cdot k} = \frac{1}{1-x^{2^{n+1}}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_82150 (n : ℕ) (x : ℝ) (hx : 0 < x ∧ x < 1) :
  (∑' k : ℕ, x^(2^(n+1) * k)) = 1 / (1 - x^(2^(n+1)))   :=  by sorry

Source