English
For natural m,n, the integral of sin^ (2m+1) x cos^n x over [a,b] equals the integral over [cos b, cos a] of u^n (1−u^2)^m.
Русский
Для натуральных m,n интеграл sin^{2m+1}x cos^n x по [a,b] равен интегралу по [cos b, cos a] от u^n (1−u^2)^m.
LaTeX
$$$$\\displaystyle \\int_{a}^{b} \\sin^{(2m+1)}x \\cos^{n}x \\,dx = \\int_{\\cos b}^{\\cos a} u^{n} (1-u^{2})^{m} \\,du.$$$$
Lean4
/-- Simplification of the integral of `sin x ^ m * cos x ^ n`, case `m` is odd. -/
theorem integral_sin_pow_odd_mul_cos_pow (m n : ℕ) :
(∫ x in a..b, sin x ^ (2 * m + 1) * cos x ^ n) = ∫ u in cos b..cos a, u ^ n * (↑1 - u ^ 2) ^ m :=
have hc : Continuous fun u : ℝ => u ^ n * (↑1 - u ^ 2) ^ m := by fun_prop
calc
(∫ x in a..b, sin x ^ (2 * m + 1) * cos x ^ n) = -∫ x in b..a, sin x ^ (2 * m + 1) * cos x ^ n := by
rw [integral_symm]
_ = ∫ x in b..a, (↑1 - cos x ^ 2) ^ m * -sin x * cos x ^ n :=
by
simp only [_root_.pow_succ, pow_mul, _root_.pow_zero, one_mul, mul_neg, neg_mul, integral_neg, neg_inj]
congr! 5
rw [← sq, ← sq, sin_sq]
_ = ∫ x in b..a, cos x ^ n * (↑1 - cos x ^ 2) ^ m * -sin x := by congr; ext; ring
_ = ∫ u in cos b..cos a, u ^ n * (↑1 - u ^ 2) ^ m :=
integral_comp_mul_deriv (fun x _ => hasDerivAt_cos x) continuousOn_sin.neg hc
