Power-reduction formula for cosine

Statement

For every real $x$, $$\cos^2 x = \frac{1 + \cos 2x}{2}, \qquad \sin^2 x = \frac{1 - \cos 2x}{2}.$$

Remarks

The addition formula gives $\cos 2x = \cos^2 x - \sin^2 x$. With the Pythagorean identity, $\cos 2x = 2 \cos^2 x - 1 = 1 - 2 \sin^2 x$. These formulas give $\int_0^{\pi} \cos^2 x \, dx = \frac{\pi}{2}$. Mathlib states the first one as Real.cos_sq.

Explanations

L1 human

A square of a cosine is a cosine of the double angle, shifted and scaled. This turns squares into first powers, which are easy to integrate.