Can the formula $\frac\pi2=(\frac21)^{1/2}(\frac{2^2}{1\cdot3})^{1/4}(\frac{2^3\cdot4}{1\cdot3^3})^{1/8}\cdots$ prove the irrationality of $\pi$?

A less known product formula for $\pi$, due to Sondow, is the following:

$$ \frac{\pi}{2}= \left(\frac{2}{1}\right)^{1/2} \left(\frac{2^2}{1\cdot3}\right)^{1/4} \left(\frac{2^3\cdot4}{1\cdot3^3}\right)^{1/8} \left(\frac{2^4\cdot4^4}{1\cdot3^6\cdot5}\right)^{1/16} \ldots $$

Is it possible to prove the irrationality of $\pi$ based on this formula, using some sort of convergence acceleration technique leading to a good irrationality measure?


Dirichlet’s approximation theorem can’t be applied here, as this product formula doesn’t give a sequence of rational approximations due to the fractional exponents.

We can show that this product formula is equivalent to the Wallis product, which does give you a sequence of rational approximations:

Let $a_n(x)$ be the product of the first $n$ terms of

$$\left(\frac{x + 1}{x}\right)^{1/2} \left(\frac{(x + 1)^2}{x(x + 2)}\right)^{1/4} \left(\frac{(x + 1)^3(x + 3)}{x(x + 2)^3}\right)^{1/8} \left(\frac{(x + 1)^4(x + 3)^4}{x(x + 2)^6(x + 4)}\right)^{1/16} \cdots.$$

Then we can see that $a_n(x)$ satisfies this recurrence:

$$a_0(x) = 1, \quad a_{n+1}(x) = \left(\frac{x + 1}{x}\right)^{1/2} \left(\frac{a_n(x)}{a_n(x + 1)}\right)^{1/2}.$$

In the limit as $n \to \infty$, this simplifies to

$$\quad a(x) = \frac{(x + 1)}{x a(x + 1)},$$

and since $\lim_{x \to \infty} a(x) = 1$, we can write

$$a(1) = \frac21 \cdot \frac1{a(2)} = \frac21 \cdot \frac23 \cdot a(3) = \cdots = \frac21 \cdot \frac23 \cdot \frac43 \cdot \frac45 \cdot \frac65 \cdot \frac67 \cdots.$$

However, since the Wallis product doesn’t qualify as lesser-known, I’d imagine that an irrationality measure proof based on it would be well known if it existed.