integral_sin_mul_cos₂ — Mathlib

English

The integral of sin x · cos x equals (cos^2 a − cos^2 b)/2; equivalently, the identity in terms of sin-cos powers.

Русский

Интеграл sin x · cos x равен (cos^2 a − cos^2 b)/2; альтернативная запись связана с степенями синуса и косинуса.

LaTeX

$$$$\\displaystyle \\int_{a}^{b} \\sin x \\cos x \\,dx = \\frac{\\cos^{2}a - \\cos^{2}b}{2}.$$$$

Lean4

/-- The integral of `sin x * cos x`, given in terms of cos².
See `integral_sin_mul_cos₁` above for the integral given in terms of sin². -/
theorem integral_sin_mul_cos₂ : ∫ x in a..b, sin x * cos x = (cos a ^ 2 - cos b ^ 2) / 2 := by
  simpa using integral_sin_pow_odd_mul_cos_pow 0 1

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