Live data from Hacker News

An Elementary Proof of Wallis’ Product Formula for Pi (2005)

fermatslibrary.com

21–23 of 23 posts

Re: An Elementary Proof of Wallis’ Product Formula for Pi (2005)

#21
post #13
post #5

I had never heard of this product formula before, so I whipped up a quick python program: http://pastebin.com/FBR8rWxv All I can say is wow, that formula slow to converge on pi. The product after 100 million terms is: 3.141592637878503 You can see that 100M terms only gets you 8 decimals of precision.

maybe I'm missing something (haven't tried to debug it), but that just results in 0. edit: Oh that's interesting. Python 2 gave me 0, Python 3 worked fine.

[deleted]

Re: An Elementary Proof of Wallis’ Product Formula for Pi (2005)

#22

In order to appreciate how phenomenally basic this derivation is: here is a derivation using Euler's infinite product expansion of the sin(x) function. http://www.jstor.org.sci-hub.cc/stable/10.4169/amer.math.mon... Then if you want your answer plug in x = π/2 inevitably Wallis formula leads to either Stirling formula or the derivation of ζ(2)=π^2/6. So for someone to solve it just by drawing some rectangles and find…

One can actually derive the Euler product for sine perfectly rigorously quite quickly, in just the manner Euler did!

(Euler is often said to have glibly moved from "sin(x)/x has roots at nonzero integer multiples of π" to "sin(x)/x = the product of (1 - x/(kπ)) for each nonzero integer k" in solving the Basel problem, simply ignoring the problem of the fact that many other functions have precisely the same zeros.

But Euler was not, in fact, always so glib in presenting this argument! For example, in Volume 1, Chapter 9 of his Introductio in Analysin Infinitorum (translation by Ian Bruce available at http://www.17centurymaths.com/contents/introductiontoanalysi...), we see that Euler argues for the product formula by noting (what would in modern notation be) that sin(x) = the imaginary part of e^(ix) = the imaginary part of (1 + ix/N)^N for infinitely large N, so that a factorization of sin(x) can be extracted from a factorization of the polynomial Im[(1 + ix/N)^N] for large N.

I'll write out in modern style the extraction of that factorization, but all the ideas are already present in the Euler:)

Let us denote Im[(1 + ix/N)^N] by f_N(x). Note that f_N is a polynomial of degree either N - 1 (if N is even) or N (if N is odd), whose degree 1 term is 1. Furthermore, its roots occur where x/N is the tangent of a multiple of π/N. Putting these together, we get that f_N(x)/x = the product of 1 - x/(N tan(kπ/N)) over the nonzero integers k in (-N/2, N/2).

As N approaches infinity, N tan(kπ/N) approaches kπ. Thus, we have that sin(x)/x = the product of 1 - x/(kπ) over the nonzero integers k.

[This last step is slightly glib, in that we've commuted limits without justification. We can rectify that by bundling together the factors where k differs only in sign, saying f_N(x)/x = the product of 1 - (x/(N tan(kπ/N)))^2 over k in (0, N/2). Now we note that the movement of the factors toward their limit is monotonic in N (considering the k-th factor to be 1 when N/2 <= k), which is sufficient justification for commuting the limits.]

Post reply on HN