Integral $\int_0^\infty \frac{\cos x}{x}\left(\int_0^x \frac{\sin t}{t}dt\right)^2dx=-\frac{7}{6}\zeta(3)$

Question

I am trying to prove this below. $$ I:=\int_0^\infty \frac{\cos x}{x}\left(\int_0^x \frac{\sin t}{t}dt\right)^2dx=-\frac{7}{6}\zeta(3) $$ where $$ \zeta(3)=\sum_{n=1}^\infty \frac{1}{n^3}. $$ I am not sure how to work with the integral over $t$ because it is from $0$ to $x$. If we can somehow write $$ \int_0^\infty \frac{\cos x}{x} \left(\int_0^\infty \frac{\sin t}{t}dt-\int_x^\infty \frac{\sin t}{t}dt \right)^2dx=\int_0^\infty \frac{\cos x}{x}\left(\frac{\pi}{2}-\int_x^\infty \frac{\sin t}{t}dt\right)^2dx. $$ I do not want to use an asymptotic expansion on the integral over $t$ from $x$ to $\infty$, I am looking for exact results. Note we can use $\int_0^\infty \frac{\sin t}{t}dt=\int_0^\infty \mathcal{L}[\sin t(s)]ds=\frac{\pi}{2}.$ Other than this approach I am not really sure how to go about this. Note by definition $$ \int_0^x \frac{\sin t}{t}dt\equiv Si(x), $$ but I'm not too sure what this definition can be used for in terms of a proof. Also note $$ \int_0^\infty \frac{\cos x}{x}dx \to \infty. $$

Answer 1

It's strange that you're unable to access that link. I do not understand that.

I accredit this to Shobit.

Anyway, what Shobit done was to write it as a triple integral.

$$I=\int_{0}^{\infty}\int_{0}^{1}\int_{0}^{1}\frac{\cos(x)\sin(xy)\sin(xz)}{xyz}dydzdx$$

$$I=1/4\int_{0}^{1}\int_{0}^{1}\int_{0}^{\infty}\frac{\cos(x(y-z+1))+\cos(x(y-z-1))-\cos(x(y+z+1))-\cos(x(y+z-1))}{xyz}dxdydz$$

Now, use the known result: $$\int_{0}^{\infty}\frac{\cos(bx)-\cos(ax)}{x}dx=\log(a/b)$$

Using this, it can now be written in terms of a log:

$$I=1/4\int_{0}^{1}\int_{0}^{1}\frac{1}{yz}\log\left(\frac{(y+z+1)(y+z-1)}{(y-z+1)(y-z-1)}\right)dydz$$

Now, integrating this w.r.t y is where the dilogs come into play:

$$I=1/4\int_{0}^{1}\frac{Li_{2}(\frac{1}{z+1})+Li_{2}(\frac{1}{z-1})-Li_{2}(\frac{-1}{z+1})-Li_{2}(\frac{1}{1-z})}{z}dz$$

Maybe you can finish it now on your own. It is now a matter of known dilog integrals. This is the bulk of it. But, if you need more I can write the rest later.