Leibniz's Series for Pi #
This theorem establishes Leibniz's series for π: The alternating sum of the reciprocals
of the odd numbers is π/4. Note that this is a conditionally rather than absolutely convergent
series. The main tool that this proof uses is the Mean Value Theorem (specifically avoiding the
Fundamental Theorem of Calculus).
Intuitively, the theorem holds because Leibniz's series is the Taylor series of arctan x
centered about 0 and evaluated at the value x = 1. Therefore, much of this proof consists of
reasoning about a function
f := arctan x - ∑ i in Finset.range k, (-(1:ℝ))^i * x^(2*i+1) / (2*i+1),
the difference between arctan and the k-th partial sum of its Taylor series. Some ingenuity is
required due to the fact that the Taylor series is not absolutely convergent at x = 1.
This proof requires a bound on f 1, the key idea being that f 1 can be split as the sum of
f 1 - f u and f u, where u is a sequence of values in [0,1], carefully chosen such that
each of these two terms can be controlled (in different ways).
We begin the proof by (1) introducing that sequence u and then proving that another sequence
constructed from u tends to 0 at +∞. After (2) converting the limit in our goal to an
inequality, we (3) introduce the auxiliary function f defined above. Next, we (4) compute the
derivative of f, denoted by f', first generally and then on each of two subintervals of [0,1].
We then (5) prove a bound for f', again both generally as well as on each of the two
subintervals. Finally, we (6) apply the Mean Value Theorem twice, obtaining bounds on f 1 - f u
and f u - f 0 from the bounds on f' (note that f 0 = 0).