English
For a natural n, the integral of sin(x)^{n+2} over [a,b] equals (sin a^{n+1} cos a − sin b^{n+1} cos b)/(n+2) + (n+1)/(n+2) ∫ sin(x)^n dx over [a,b].
Русский
Для натурального n интеграл sin(x)^{n+2} по [a,b] равен [sin a^{n+1} cos a − sin b^{n+1} cos b]/(n+2) + (n+1)/(n+2)∫ sin(x)^n dx.
LaTeX
$$$$\\displaystyle \\int_{a}^{b} \\sin^{(n+2)}x \\,dx = \\frac{\\sin a^{n+1} \\cos a - \\sin b^{n+1} \\cos b}{n+2} + \\frac{n+1}{n+2}\\int_{a}^{b} \\sin^{n}x \\,dx.$$$$
Lean4
/-- The reduction formula for the integral of `sin x ^ n` for any natural `n ≥ 2`. -/
theorem integral_sin_pow :
(∫ x in a..b, sin x ^ (n + 2)) =
(sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b) / (n + 2) + (n + 1) / (n + 2) * ∫ x in a..b, sin x ^ n :=
by
field_simp
convert eq_sub_iff_add_eq.mp (integral_sin_pow_aux n) using 1
ring
