sequences and series - Prove $int_0^{pi/2} J_0 (cos x) dx=frac{pi}{2} left(J_0 left(frac{1}{2} right)right)^2$

I got curious about this integral because we have the following identity:

$$\frac{2}{\pi}\int_0^{\pi/2} \cos (x\cos t) dt=J_0(x)$$

So we have an interesting (if useless) symmetry:

$$\int_0^{\pi/2} J_0 (\cos x) dx=\frac{2}{\pi}\int_0^{\pi/2}\int_0^{\pi/2} \cos (\cos x \cos t) ~dt~dx=\int_0^{\pi/2} J_0 (\cos t) dt$$

Wolfram Alpha doesn't show a closed form for this integral. However, if we use the series for the Bessel function:

$$J_0(x)=\sum_{k=0}^\infty \frac{(-1)^k x^{2k}}{4^kk!^2}$$

And the known closed form for the family of integrals:

$$\int_0^{\pi/2} \cos^{2k} (x) dx=\frac{\sqrt{\pi}}{2}\frac{\Gamma \left(k+\frac{1}{2} \right)}{k!}$$

We obtain:

$$\int_0^{\pi/2} J_0 (\cos x) dx=\frac{\sqrt{\pi}}{2} \sum_{k=0}^\infty \frac{(-1)^k \Gamma \left(k+\frac{1}{2} \right)}{4^kk!^3}$$

Wolfram Alpha evaluates this series, giving a closed form for the integral:

$$\int_0^{\pi/2} J_0 (\cos x) dx=\frac{\pi}{2} \left(J_0 \left(\frac{1}{2} \right)\right)^2=1.3834405\dots$$

This agrees with the numerical value. However, I have not been able to show this myself.

How do we prove this closed form? Is there a more general case, involving Bessel functions of order $n$?

Answer

$$J_0 \left ( x \right )^2 = \sum_{m=0}^{\infty} \sum_{n=0}^{\infty} \frac{(-1)^{m+n}}{m!^2 n!^2} \frac{x^{2 (m+n)}}{2^{2 (m+n)}}$$

or, looking at coefficients of $x^{2 k}$, i.e., $m+n=k$:

$$J_0 \left ( x \right )^2 = \sum_{k=0}^{\infty} \sum_{m=0}^k \frac{(-1)^k}{m!^2 (k-m)!^2} \frac{x^{2 k}}{2^{2 k}}$$

Now,

$$\sum_{m=0}^k \frac{1}{m!^2 (k-m)!^2} = \frac1{k!^2} \binom{2 k}{k}$$

Thus,

$$J_0 \left ( \frac12 \right )^2 = \sum_{k=0}^{\infty} \frac{(-1)^k (2 k)!}{2^{4 k} k!^4}$$

which you will find is equivalent to the sum you have above.

NB

$$\Gamma \left (k+\frac12 \right ) = \frac{(2 k)! \sqrt{\pi}}{2^{2 k} k!}$$