複素積分6

今回はこちらの積分botさんの積分
https://twitter.com/integralsbot/status/1432926358229839878?s=21
を解説します。

$\displaystyle\log(x-i\log\sin x)=\frac{1}{2}\log(x^2+\log^2\sin x)-i\tan^{-1}\frac{\log\sin x}{x}$
より

$\displaystyle\int_0^\pi\tan^{-1}\frac{\log\sin x}{x}dx=-\Im\int_0^\pi\log(x-i\log\sin x)dx$
$=-\displaystyle\frac{1}{2}\Im\int_0^{2\pi}\log(\frac{x}{2}-i\log\sin\frac{x}{2})dx$
$=-\displaystyle\frac{1}{2}\Im\oint_{C:z=e^{ix}}\log(-i\log\sqrt z-i\log\frac{\sqrt z-{\sqrt z}^{-1}}{2i})\frac{dz}{iz}$
$=-\displaystyle\frac{1}{2}\Im\oint_C\log(\frac{1}{i}\log\frac{z-1}{2i})\frac{dz}{iz}$
$=-\displaystyle\pi\Im\lim_{z→0}\log(\frac{1}{i}\log\frac{z-1}{2i})$
$=-\displaystyle\pi\Im\log(\frac{1}{i}\log\frac{e^{\frac{\pi}{2} i}}{2})$
$=-\displaystyle\pi\Im\log(\frac{\pi}{2}+i\log2)$
$=-\displaystyle\pi\tan^{-1}\frac{2\log2}{\pi}$