English
The integral of cos^3 over [a,b] equals sin a − sin b − (sin^3 a − sin^3 b)/3.
Русский
Интеграл cos^3 по [a,b] равен sin a − sin b − (sin^3 a − sin^3 b)/3.
LaTeX
$$$$\\displaystyle \\int_{a}^{b} \\cos^{3}x \\,dx = \\sin a - \\sin b - \\frac{\\sin^{3}a - \\sin^{3}b}{3}. $$$$
Lean4
/-- Simplification of the integral of `sin x ^ m * cos x ^ n`, case `n` is odd. -/
theorem integral_sin_pow_mul_cos_pow_odd (m n : ℕ) :
(∫ x in a..b, sin x ^ m * cos x ^ (2 * n + 1)) = ∫ u in sin a..sin b, u ^ m * (↑1 - u ^ 2) ^ n :=
have hc : Continuous fun u : ℝ => u ^ m * (↑1 - u ^ 2) ^ n := by fun_prop
calc
(∫ x in a..b, sin x ^ m * cos x ^ (2 * n + 1)) = ∫ x in a..b, sin x ^ m * (↑1 - sin x ^ 2) ^ n * cos x :=
by
simp only [_root_.pow_zero, _root_.pow_succ, mul_assoc, pow_mul, one_mul]
congr! 5
rw [← sq, ← sq, cos_sq']
_ = ∫ u in sin a..sin b, u ^ m * (1 - u ^ 2) ^ n :=
integral_comp_mul_deriv (fun x _ => hasDerivAt_sin x) continuousOn_cos hc
