Real.tendsto_sum_pi_div_four

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

The theorem named "Real.tendsto_sum_pi_div_four" is also known as "Leibniz's series for `π`". It states that the limit as `k` tends to infinity of the sum, from `i = 0` to `k`, of `(-1)^i / (2*i + 1)` equals `π/4`. This sum is an alternating sum of the reciprocals of odd numbers. The proof of this theorem uses Abel's limit theorem to extend the Maclaurin series of the arctangent function to 1. In simpler words, as you add up more and more terms in this special alternating series, you get closer and closer to `π/4`.

More concisely: The limit as n goes to infinity of the sum, from i = 0 to i = n, of (-1)^i / (2*i + 1) equals π/4.