Q:

A conjectured closed form of $\int\limits_0^\infty\frac{x-1}{\sqrt{2^x-1}\ \ln\left(2^x-1\right)}dx$

Consider the following integral:
$$\mathcal{I}=\int\limits_0^\infty\frac{x-1}{\sqrt{2^x-1}\ \ln\left(2^x-1\right)}dx.$$
I tried to evaluate $\mathcal{I}$ in a closed form (both manually and using Mathematica), but without success. 
However, if WolframAlpha is provided with a numerical approximation $\,\mathcal{I}\approx 3.2694067500684...$, it returns a possible closed form: 
$$\mathcal{I}\stackrel?=\frac\pi{2\,\ln^2 2}.$$
Further numeric caclulations show that this value is correct up to at least $10^3$ decimal digits. So, I conjecture that this is the exact value of $\mathcal{I}$.

Question: Is this conjecture correct?

A:

Sub $u=\log{(2^x-1)}$.  Then $x=\log{(1+e^u)}/\log{2}$, $dx = (1/\log{2}) (du/(1+e^{-u})$.  The integral then becomes
$$\begin{align}\frac{1}{\log{2}} \int_{-\infty}^{\infty} \frac{du}{1+e^{-u}} e^{-u/2} \frac{\frac{\log{(1+e^u)}}{\log{2}}-1}{u} = \frac{1}{2\log^2{2}} \int_{-\infty}^{\infty} \frac{du}{\cosh{(u/2)}} \frac{\log{(1+e^u)}-\log{2}}{u}\\ = \underbrace{\frac{1}{2\log^2{2}} \int_{-\infty}^{0} \frac{du}{\cosh{(u/2)}} \frac{\log{(1+e^u)}-\log{2}}{u}}_{u\rightarrow -u} \\+ \frac{1}{2\log^2{2}} \int_{0}^{\infty} \frac{du}{\cosh{(u/2)}} \frac{\log{(1+e^u)}-\log{2}}{u}\\ = \underbrace{-\frac{1}{2\log^2{2}} \int_{0}^{\infty} \frac{du}{\cosh{(u/2)}} \frac{\log{(1+e^{-u})}-\log{2}}{u}}_{\log{(1+e^{-u})} = \log{(1+e^u)}-u}\\+ \frac{1}{2\log^2{2}} \int_{0}^{\infty} \frac{du}{\cosh{(u/2)}} \frac{\log{(1+e^u)}-\log{2}}{u}\\ \end{align}$$
The nasty pieces of the integral cancel, and we are left with
$$ \frac{1}{2\log^2{2}}\int_{0}^{\infty} \frac{du}{\cosh{(u/2)}} = \frac{\pi}{2 \log^2{2}} $$
as correctly conjectured.

A:

$\newcommand{\angles}[1]{\left\langle #1 \right\rangle}%
 \newcommand{\braces}[1]{\left\lbrace #1 \right\rbrace}%
 \newcommand{\bracks}[1]{\left\lbrack #1 \right\rbrack}%
 \newcommand{\dd}{{\rm d}}%
 \newcommand{\ds}[1]{\displaystyle{#1}}%
 \newcommand{\expo}[1]{{\rm e}^{#1}}%
 \newcommand{\ic}{{\rm i}}%
 \newcommand{\imp}{\Longrightarrow}%
 \newcommand{\pars}[1]{\left( #1 \right)}%
 \newcommand{\pp}{{\cal P}}%
 \newcommand{\ul}[1]{\underline{#1}}%
 \newcommand{\verts}[1]{\left\vert #1 \right\vert}
 \newcommand{\yy}{\Longleftrightarrow}$
$\ds{%
{\cal I}
\equiv
\int\limits_{0}^{\infty}
{x - 1
 \over
 \sqrt{\vphantom{\large A}2^{x} - 1\,}\,\ln\pars{2^{x} - 1}}\,\dd x:\ {\large ?}}$
With the change of variables
$z \equiv 2^{x} - 1\yy x = \ln\pars{1 + z}/\ln\pars{2},\ {\cal I}$ is reduced to
$$
{\cal I}
=
{1 \over \ln^{2}\pars{2}}
\int\limits_{0}^{\infty}{\ln\pars{1 + z} - \ln\pars{2} \over z^{1/2}\,\pars{1 + z}\,\ln\pars{z}}
\,\dd z
$$
Now, we split the integral from $\pars{0, 1}$ and from $\pars{1, \infty}$. In the second one, we makes the change $z \to 1/z$ such that we are left with an integration over $\pars{0, 1}$:
\begin{align}
{\cal I}
&=
{1 \over \ln^{2}\pars{2}}
\int\limits_{0}^{1}{\ln\pars{1 + z}  - \ln\pars{2} \over z^{1/2}\,\pars{1 + z}\,\ln\pars{z}}
\,\dd z
+
{1 \over \ln^{2}\pars{2}}\int\limits_{0}^{1}
{\ln\pars{1 + 1/z} - \ln\pars{2} \over z^{-1/2}\,\pars{1 + 1/z}\,\bracks{-\ln\pars{z}}}
\,{\dd z \over z^{2}}
\\[3mm]&=
{1 \over \ln^{2}\pars{2}}
\int\limits_{0}^{1}{\ln\pars{1 + z} - \ln\pars{2} \over z^{1/2}\,\pars{1 + z}\,\ln\pars{z}}
\,\dd z
-
{1 \over \ln^{2}\pars{2}}\int\limits_{0}^{1}
{\ln\pars{1 + z} - \ln\pars{z} - \ln\pars{2}
 \over
 z^{1/2}\,\pars{1 + z}\,\ln\pars{z}}\,\dd z
\\[3mm]&=
{1 \over \ln^{2}\pars{2}}
\int\limits_{0}^{1}{1 \over z^{1/2}\,\pars{1 + z}}
\,\dd z\,,
\quad
\pars{~\mbox{Let's}\quad r \equiv z^{1/2}\yy\ z = r^{2}~}
\\[3mm]&= 
{2 \over \ln^{2}\pars{2}}
\underbrace{\quad\int\limits_{0}^{1}{\dd r \over r^{2} + 1}\quad}
_{\ds{\arctan\pars{1}\ =\ {\pi \over 4}}}
=
\color{#ff0000}{\Large{\pi \over 2\ln^{2}\pars{2}}}
\end{align}

A:

Let $\tan^2t=2^x-1\;\Rightarrow\;x=\dfrac{\ln(1+\tan^2t)}{\ln 2}\;\Rightarrow\;dx=\dfrac{2\tan t\sec^2t\ dt}{(1+\tan^2t)\ln 2}$ and the corresponding region is $0<t<\dfrac\pi2$. Using identity $\sec^2t=1+\tan^2t$, then the integral turns out to be
$$
\mathcal{I}=\frac{1}{\ln^22}\int_0^{\Large\frac\pi2}\frac{2\ln(\sec t)-\ln2}{\ln (\tan t)}\ dt.\tag1
$$
Now, using property
$$
\int_b^af(x)\ dx=\int_b^af(a+b-x)\ dx
$$
equation $(1)$ becomes
$$
\mathcal{I}=\frac{1}{\ln^22}\int_0^{\Large\frac\pi2}\frac{2\ln(\csc t)-\ln2}{\ln (\cot t)}\ dt.\tag2
$$
Adding $1$ and $2$ yields
$$
\begin{align}
2\mathcal{I}&=\frac{1}{\ln^22}\int_0^{\Large\frac\pi2}\left(\frac{2\ln(\sec t)-\ln2}{\ln (\tan t)}+\frac{2\ln(\csc t)-\ln2}{\ln (\cot t)}\right)\ dt\\
&=\frac{1}{\ln^22}\int_0^{\Large\frac\pi2}\left(\frac{2\ln\left(\dfrac{1}{\cos t}\right)-\ln2}{\ln (\tan t)}+\frac{2\ln\left(\dfrac{1}{\sin t}\right)-\ln2}{\ln \left(\dfrac{1}{\tan t}\right)}\right)\ dt\\
&=\frac{1}{\ln^22}\int_0^{\Large\frac\pi2}\left(\frac{-2\ln(\cos t)-\ln2}{\ln (\tan t)}+\frac{2\ln(\sin t)+\ln2}{\ln (\tan t)}\right)\ dt\\
&=\frac{2}{\ln^22}\int_0^{\Large\frac\pi2}\frac{\ln(\sin t)-\ln(\cos t)}{\ln \left(\dfrac{\sin t}{\cos t}\right)}\ dt\\
\mathcal{I}&=\frac{1}{\ln^22}\int_0^{\Large\frac\pi2}\ dt\\\\
\int_0^\infty\frac{x-1}{\sqrt{2^x-1}\ \ln\left(2^x-1\right)}dx&=\large\color{blue}{\frac{\pi}{2\ln^22}}.\qquad\qquad\qquad\blacksquare
\end{align}
$$

