Documentation

Mathlib.Data.Real.Pi.Leibniz

Leibniz's series for π #

theorem Real.tendsto_sum_pi_div_four :
Filter.Tendsto (fun (k : ) => iFinset.range k, (-1) ^ i / (2 * i + 1)) Filter.atTop (nhds (Real.pi / 4))

Leibniz's series for π. The alternating sum of odd number reciprocals is π / 4, proved by using Abel's limit theorem to extend the Maclaurin series of arctan to 1.