Pi!

[kbuzzard]

@dorhinj defined exp and cos and sin as power series on the complex numbers, and proved that these series converged. However I don't think anyone has proved that these functions are continuous! The reason I am interested in this is that one definition of pi is that it's two times the smallest positive real r such that cos(r)=0. However, to make this definition work we need that cos is continuous and we need the intermediate value theorem and we need the fact that cos takes negative values. We just convinced ourselves that cos(2)<0 because it's 1-2+2/3-2^6/6!+2^8/8!-... and the sum is alternating and the absolute values of the terms are decreasing in value from 2^6/6! onwards, so cos(2)=-1/3-2^6/6!+...<-1/3<0. Now we need that cos is continuous (and everyone seems to be a bit hazy about how this works, although 2nd years and above all know that a power series is actually differentiable within its radius of convergence, so certainly continuous), and once we have that we should be able to define pi.

[kbuzzard]

Current state: still don't continuity of cos -- @dorhinj how much work is this to PR? Can I help?

[kbuzzard]

Update: exp is hopefully on the way!