What is the real part of $\int_{0}^{\pi/2} \frac{x^2}{x^2+\log ^2(-2\cos x)} \:\mathrm{d}x$?

Question

This is a new integral that I propose to evaluate in closed form: $$ {\mathfrak{R}} \int_{0}^{\pi/2} \frac{x^2}{x^2+\log ^2(-2\cos x)} \:\mathrm{d}x$$ where $\Re$ denotes the real part and $\log (z)$ denotes the principal value of the logarithm defined for $z \neq 0$ by $$ \log (z) = \ln |z| + i \mathrm{Arg}z, \quad -\pi <\mathrm{Arg} z \leq \pi.$$

Answer 1

$$\color{blue}{\Re\int_{0}^{\pi/2} \frac{x^2}{x^2+\log ^2(-2\cos x)}dx = \frac{\pi }{8}\left( {1 - \ln 2 - \gamma } \right)}$$

---

For a proof, I will continue from $$\tag{4} - 8\Re I + 2\pi J = \pi \ln 2 - \pi$$ in this question. where $$J=\int_0^\infty {\frac{1}{{{x^2} + {\pi ^2}}}\left[ { - \frac{x}{{1 - {e^{ - x}}}} + \ln ({e^x} - 1)} \right]dx}$$ Integration by part shows $$J = -\pi \int_0^\infty {\arctan x\frac{{{e^{\pi x}}x}}{{{{\left( {{e^{\pi x}} - 1} \right)}^2}}}dx} $$ Invoke the Binet second formula: $$\ln\Gamma(z) = (z-\frac{1}{2})\ln z - z + \frac{\ln(2\pi)}{2}+2z\int_0^\infty \frac{\arctan t}{e^{2\pi t z} - 1} dt$$ The value of $J$ immdiately follows from differentiating with respect to $z$, and then set $z = 1/2$: $$J = -\frac{\gamma}{2}$$

I hope someone can explain reminiscence of this result to another question.

Answer 2

I don't think a closed form exists after computing that integral numerically in Mathematica, and looking up in the Inverse Symbolic Calculator. It is approximately equal to: $-0.10617124113817\ldots$ If you need more digits just ask.