The double-exponential maps and their change-of-variable identities

Differentiating $s(t)$ and $c(t)$ from their exponential formulas gives $s^{\mathrm{\prime }}(t)=c(t)>0$. By [F6], multiplying the defining quotient $\sinh u\mathrm{/}\cosh u$ by $e^u\mathrm{/}{e}^u$ gives $\tanh u=(e^{2u}-1)\mathrm{/}(e^{2u}+1)$, with positive denominator. Differentiating this quotient using [F7] gives ${\tanh }^{\mathrm{\prime }}(u)=1\mathrm{/}{\cosh }^{2}u>0$. The chain rule therefore gives the three positive derivatives in [F1]; [F5] makes each map strictly increasing.

By [F2], $s(t)\to \pm \mathrm{\infty }$ as $t\to \pm \mathrm{\infty }$. Thus $\tanh ((\pi \mathrm{/}2)s(t))\to \pm 1$, $\exp ((\pi \mathrm{/}2)s(t))$ tends to $0$ and $+\mathrm{\infty }$ at the two ends, and $\sinh ((\pi \mathrm{/}2)s(t))\to \pm \mathrm{\infty }$. Continuity, strict increase, and these endpoint limits prove the stated ranges and bijectivity.

Fix $T>0$. The displayed derivatives in [F1] are continuous by their exponential formulas, so [F8] makes them Riemann integrable on $[-T,T]$. The relevant $f$ is continuous on the nondegenerate compact image interval, so [F3] gives ${\int }_{x(-T)}^{x(T)}f(x)dx={\int }_{-T}^T\mathrm{\Phi }(t)dt$. Applying the same identity to $\mathrm{\mid }f\mathrm{\mid }$ shows that the truncated absolute integrals equal ${\int }_{-T}^T\mathrm{\mid }\mathrm{\Phi }(t)\mathrm{\mid }dt$. The two nonnegative absolute integrals on either side of $x(0)$ increase and are bounded by ${\int }_{\mathbb{R}}\mathrm{\mid }\mathrm{\Phi }\mathrm{\mid }$, so each converges separately. Since the endpoints tend to the target endpoints by step 2.1, the target integral converges absolutely, and taking limits in the signed identity proves the asserted equality.