English
For natural m,n, the integral of sin^m x · cos x^{2n+1} over [a,b] equals the integral over [sin a, sin b] of u^m (1−u^2)^n.
Русский
Для натуральных m,n интеграл sin^m x · cos x^{2n+1} по [a,b] равен интегралу по [sin a, sin b] от u^m (1−u^2)^n.
LaTeX
$$$$\\displaystyle \\int_{a}^{b} \\sin^{m}x \\cos^{2n+1}x \\,dx = \\int_{\\sin a}^{\\sin b} u^{m} (1-u^{2})^{n} \\,du.$$$$
Lean4
/-- The integral of `sin x * cos x`, given in terms of sin².
See `integral_sin_mul_cos₂` below for the integral given in terms of cos². -/
@[simp]
theorem integral_sin_mul_cos₁ : ∫ x in a..b, sin x * cos x = (sin b ^ 2 - sin a ^ 2) / 2 := by
simpa using integral_sin_pow_mul_cos_pow_odd 1 0