A closed form for $\int_0^\infty\ln x\cdot\ln\left(1+\frac1{2\cosh x}\right)dx$ Is it possible to evaluate this integral in a closed form?
$$\int_0^\infty\ln x\cdot\ln\left(1+\frac1{2\cosh x}\right)dx=\int_0^\infty\ln x\cdot\ln\left(1+\frac1{e^{-x}+e^x}\right)dx$$
I tried to evaluate it with a CAS, and looked up in integral tables, but was not successful.
 A: Define
$$ I(\alpha) = \int_{0}^{\infty} \log x \log(1 - e^{-\alpha x}) \, dx. $$
Integrating by parts, followed by the substitution $\alpha x \mapsto x$, we have
\begin{align*}
I(\alpha)
&= \alpha \int_{0}^{\infty} \frac{x - x\log x}{e^{\alpha x} - 1} \, dx \\
&= \frac{1}{\alpha} \int_{0}^{\infty} \frac{(1+\log \alpha) x - x \log x}{e^{x} - 1} \, dx\\
&= \frac{1}{\alpha} \left\{ (1+\log\alpha)\zeta(2) - \left.\frac{d \zeta(s)\Gamma(s)}{s}\right|_{s=2} \right\}\\
&= \frac{1}{\alpha} \left\{ (\gamma+\log\alpha)\zeta(2) - \zeta'(2) \right\}.
\end{align*}
Then it follows that
\begin{align*}
\int_{0}^{\infty} \log x \log \left( 1 + \frac{1}{2\cosh x} \right) \, dx
&= \int_{0}^{\infty} \log x \log \left( \frac{1 - e^{-3x}}{1 - e^{-x}} \cdot \frac{1 - e^{-2x}}{1 - e^{-4x}} \right) \, dx \\
&= I(2) + I(3) - I(1) - I(4) \\
&= \frac{5}{12} \zeta'(2) - \frac{5}{72}\gamma\pi^{2} + \frac{1}{18}\pi^{2} \log (3).
\end{align*}
Plugging some identities relating $\zeta'(2)$ and the Glaisher-Kinkelin constant $A$, this reduces to Vladimir's answer.
Addendum - Something you might want to know:
The following identity played the key role in this proof.
$$ \int_{0}^{\infty} \frac{x^{s-1}}{e^{x} - 1} \, dx = \Gamma(s)\zeta(s), $$
which holds for $\Re s > 1$.
