lean_workbook_plus_53967

Proved

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

Find the closed form for the general case: $\sum_{n=0}^\infty \frac{\binom{2n}{n}}{4^n(n+1)^k}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_53967 (k : ℕ) : ∃ (f : ℕ → ℝ), ∀ (n : ℕ), (∑' n : ℕ, (Nat.choose (2 * n) n) / (4 ^ n * (n + 1) ^ k)) = f k   :=  by sorry

Source