Logarithmic sine integral (${\int }_0^1\sin (a\log x)/\log xdx=\arctan a$)

For every real $a$, define $I(a)={\int }_0^1\sin (a\log x)/\log xdx$. The apparent endpoint singularity at $x=1$ is removable, with limit $a$, and the bound $|\sin (a\log x)/\log x|\le |a|$ ensures integrability. Differentiation under the integral sign is justified by the integrable bound $|\cos (a\log x)|\le 1$ on the parameter derivative. Thuswhere $x=e^{-t}$ and the last integral is a Laplace transform. Since $I(0)=0$, integrating with respect to $a$ gives $I(a)=\arctan a$. This obtains an integral with a logarithmic denominator by differentiating away that denominator, then restoring the parameter dependence with one elementary antiderivative.