English
For any natural n, the integral of cos^{n+2} over [a,b] equals the boundary term plus a multiple of the integral of cos^n over [a,b], with a factor involving n+2.
Русский
Для любого натурального n интеграл cos^{n+2} по [a,b] равен граничному члену плюс множитель на интеграл cos^n по [a,b], с коэффициентом, зависящим от n+2.
LaTeX
$$$$\\displaystyle \\int_{a}^{b} \\cos^{(n+2)}x \,dx = \\frac{\\cos b^{n+1}\\sin b - \\cos a^{n+1}\\sin a}{n+2} + \\frac{n+1}{n+2}\\int_{a}^{b} \\cos^{n}x \,dx.$$$$
Lean4
/-- The reduction formula for the integral of `cos x ^ n` for any natural `n ≥ 2`. -/
theorem integral_cos_pow :
(∫ x in a..b, cos x ^ (n + 2)) =
(cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a) / (n + 2) + (n + 1) / (n + 2) * ∫ x in a..b, cos x ^ n :=
by
field_simp
convert eq_sub_iff_add_eq.mp (integral_cos_pow_aux n) using 1
ring
