求证：
\[ \int_{0}^{\frac{\pi}{2}}{x\ln{\sin{x}}\ln{\cos{x}}dx}=\frac{(\pi\ln{2})^{2}}{8}-\frac{\pi^{4}}{192} \]
证明：
首先，我们设
\[ A=\int_{0}^{\frac{\pi}{2}}{x\ln{\sin{x}}\ln{\cos{x}}dx} \]
很显然，
\[ A=\frac{\pi}{4}\int_{0}^{\frac{\pi}{2}}{\ln{\sin{x}}\ln{\cos{x}}dx}\]
所以，只需要求
\[ B=\int_{0}^{\frac{\pi}{2}}{\ln{\sin{x}}\ln{\cos{x}}dx}\]
由傅里叶级数不难得到
\[ \ln{(2\cos{\frac{x}{2}})}=\sum_{n=1}^{\infty}{(-1)^{n-1}\frac{\cos{nx}}{n}}, \qquad -\pi<x<\pi \]
由$2x$替换$x$,得到
\[ \ln{(2\cos{x})}=\sum_{n=1}^{\infty}{(-1)^{n-1}\frac{\cos{2nx}}{n}}, \qquad -\frac{\pi}{2}<x<\frac{\pi}{2} \]
而另一方面
\begin{align*}
\int_{0}^{\frac{\pi}{2}}{\cos{2nx}\ln{\sin{x}}dx}&=\int_{0}^{\frac{\pi}{2}}{\ln{\sin{x}}d\frac{\sin{2nx}}{2n}}\\
&=\frac{1}{2n}\sin{2nx}\cdot\ln{\sin{x}}|_{0}^{\frac{\pi}{2}}-\frac{1}{2n}\int_{0}^{\frac{\pi}{2}}{\frac{\cos{x}\cdot\sin{2nx}}{\sin{x}}dx}\\
&=-\frac{1}{4n}\int_{0}^{\frac{\pi}{2}}{\frac{\sin{(2n+1)x}+\sin{(2n-1)x}}{\sin{x}}dx}\\
&=-\frac{\pi}{4n}
\end{align*}
所以
\begin{align*}
\int_{0}^{\frac{\pi}{2}}{\ln{2\cos{x}}\cdot\ln{\sin{x}}dx}&=\sum_{n=1}^{\infty}{(-1)^{n}\frac{\pi}{4n^2}}\\
&=B+\ln{2}\cdot\int_{0}^{\frac{\pi}{2}}{\ln{\sin{x}}dx}
\end{align*}
马上看到
\[ B=\frac{\pi}{2}\ln^{2}{2}-\frac{1}{48}{\pi^{3}} \]
\[ A= \frac{(\pi\ln{2})^{2}}{8}-\frac{\pi^{4}}{192} \]
Done!

$ \square$

——————————————————————————————————————————————————————

说实话，那个

\[ \ln{(2\cos{\frac{x}{2}})}=\sum_{n=1}^{\infty}{(-1)^{n-1}\frac{\cos{nx}}{n}}, \qquad -\pi<x<\pi \]

真心很有用，用这个可以算出下面结果

\[ \int_{0}^{\frac{\pi}{2}}{\ln^{2}{\sin{x}}dx}=\int_{0}^{\frac{\pi}{2}}{\ln^{2}{\cos{x}}dx}=\frac{\pi^3}{24}+\frac{\pi}{2}\ln^{2}{2} \]

只要考虑傅里叶级数正交就好。