integral_sin_mul_cos₁ — Mathlib

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

Похожие утверждения