3-in-1 coffee

Let us simplify our integral:

$\int_0^{\pi/2} \ln(\cos x \sin x) \ln \tan x \ dx = \int_0^{\pi/2} (\ln \cos x + \ln \sin x)(\ln \sin x - \ln \cos x) \ dx = \int_0^{\pi/2} \ln^2 \cos x - \ln^2 \sin x \ dx$

Initially, this seems to be a very difficult integral (perhaps requiring techniques beyond elementary calculus). However, inspecting the interval over which the integral is taken suggests that $\displaystyle \int_0^{\pi/2} \ln^2 \cos x \ dx = \int_0^{\pi/2} \ln^2 \sin x \ dx$ , since $\displaystyle \int_0^{\pi/2} \cos x \ dx = \int_0^{\pi/2} \sin x \ dx$ .

To rigorously prove this, we use u-substitution and the identity $\cos x = \sin(\dfrac{\pi}{2} - x)$ to obtain

$\begin{aligned} \int_0^{\pi/2} \ln^2 \cos x \ dx &= \int_0^{\pi/2} \ln^2 \sin(\dfrac{\pi}{2} - x) \ dx & (\text{Let } u = \dfrac{\pi}{2} - x) \\ &= \int_{\pi/2}^0 -\ln^2 \sin u \ du & (\text{Reverse integral limits}) \\ &= \int_0^{\pi/2} \ln^2 \sin u \ du \end{aligned}$

which verifies our hypothesis. Thus,

$\int_0^{\pi/2} \ln^2 \cos x - \ln^2 \sin x \ dx = \int_0^{\pi/2} \ln^2 \cos x \ dx - \int_0^{\pi/2} \ln^2 \sin x \ dx = \boxed{0}$