Prove that $\int_0^\infty \frac{\sin^2{(x\sin x)}}{x^2}dx=1$.

Question

Let $I=\int_0^\infty \frac{\sin^2{(x\sin x)}}{x^2}dx$. Prove that $I=1$.

Desmos shows that $\sum\limits_{k=0}^{100}\int_{k\pi}^{(k+1)\pi}\frac{\sin^2(x\sin{x})}{x^2}dx=0.9984\dots$ and $\sum\limits_{k=0}^{10000}\int_{k\pi}^{(k+1)\pi}\frac{\sin^2(x\sin{x})}{x^2}dx=0.999987\dots$.

So I think it's a safe bet that $I=1$.

Context

I recently learned that $\int_0^\infty \frac{\sin{(x\sin{x})}}{x^2}dx=\pi/2$. On a whim, I squared the numerator, and then to my surprise this new integral $\int_0^\infty \frac{\sin^2{(x\sin x)}}{x^2}dx$ seems to also have a closed form - in fact $1$, the simplest closed form of all.

My attempt

There are lots of ways to show that $\int_0^\infty\frac{\sin^2 x}{x^2} dx=\pi/2$. I've been trying to apply these to $I$. For example I tried to use integration by parts, but the fact that $I$ has sine within sine makes things difficult.

Answer 1

Similar to Gary's approach to the other integral, we can use the Jacobi–Anger expansion $$\cos(z \sin \theta) = J_{0}(z) + 2 \sum_{k=1}^{\infty} J_{2k}(z) \cos(2 k \theta) $$ to write the integral as $$\begin{align} \int_0^\infty \frac{\sin^2{(x\sin x)}}{x^2} \, \mathrm dx &= \int_{0}^{\infty} \frac{1-\cos(2x \sin x)}{2x^{2}} \, \mathrm dx \\ &= \frac{1}{2} \int_{0}^{\infty} \frac{1-J_{0}(2x)}{x^{2}} \, \mathrm dx - \sum_{k=1}^{\infty} \int_{0}^{\infty} \frac{J_{2k}(2x) \cos(2kx)}{x^{2}} \, \mathrm dx. \end{align}$$

For basically the same reason that I explained in my answer to your other question, the integral $$\int_{0}^{\infty} \frac{J_{2k}(2x) \cos(2kx)}{x^{2}} \, \mathrm dx$$ vanishes for all $k \in \mathbb{Z}_{\ge 1}$.

Therefore, using the fact that $J_{0}(x)$ and $J_{0}(x) -1$ have the same Mellin transform but different regions of convergence (which I showed in the addendum to my answer here using Ramanujan's Master Theorem), we have $$ \begin{align} \int_0^\infty \frac{\sin^2{(x\sin x)}}{x^2} \, \mathrm dx &= \frac{1}{2} \int_{0}^{\infty}\frac{1- J_{0}(2x)}{x^{2}} \, \mathrm dx \\ &= \int_{0}^{\infty} \frac{1-J_{0}(u)}{u^{2}} \, \mathrm du \\ &= \lim_{s \to -1} \int_{0}^{\infty} \left(1-J_{0}(u) \right)u^{s-1} \, \mathrm du \\ &= -\lim_{s \to -1} \frac{2^{s-1}\Gamma \left(\frac{s}{2} \right)}{\Gamma \left(1-\frac{s}{2} \right)} \\ &= -\frac{2^{-2} \, \Gamma \left(- \frac{1}{2} \right)}{\Gamma\left(\frac{3}{2} \right)} \\ &= -\frac{1}{4} \frac{\Gamma \left(\frac{1}{2} \right)}{\left(- \frac{1}{2} \right)} \frac{1}{\frac{1}{2} \, \Gamma \left(\frac{1}{2} \right)} \\ &= 1. \end{align}$$

Answer 2

Too long for a comment

Starting from @Random Variable's nice answer, we can even compute $$I(a,b)=\int_a^b \frac{\sin^2{(x\sin (x))}}{x^2}\,dx$$ since $$\int \frac{1-J_0(u)}{u^2}\,du= \frac 1 u \left(\, _1F_2\left(-\frac{1}{2};\frac{1}{2},1;-\frac{u^2}{4}\right)-1 \right)$$ $$\int_0^t \frac{1-J_0(u)}{u^2}\,du=\frac 1 t \left(\, _1F_2\left(-\frac{1}{2};\frac{1}{2},1;-\frac{t^2}{4}\right)-1 \right)$$ whose asymptotic is $$\int_0^t \frac{1-J_0(u)}{u^2}\,du=1-\frac 1 t +\frac{\cos (t)-\sin (t)}{\sqrt{\pi }\, t^{5/2}}+\frac{21 (\sin (t)+\cos (t))}{8 \sqrt{\pi } \,t^{7/2}}+\cdots$$