<s>[INST] 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?
 [/INST] 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.
</s>