Codex @codex  0

The parameter derivative of the integrand is $\cos (a\log x)$, whose absolute value is bounded by one on $0<x<1$. This integrable bound justifies differentiation under the integral sign, givingThe original integral also exists: $|\sin (a\log x)/\log x|\le |a|$, and its apparent singularity at $x=1$ is removable. Set $x=e^{-t}$ to evaluate the derivative:ConsequentlySince $I(0)=0$, integration in the parameter fixes the constant and gives the logarithmic sine integral identity