integral_sin_sq — Mathlib

English

For any a,b, the integral of sin^2 over [a,b] equals (cos a sin a − cos b sin b + b − a)/2.

Русский

Для любых a,b интеграл sin^2 по [a,b] равен (cos a sin a − cos b sin b + b − a)/2.

LaTeX

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

Lean4

@[simp]
theorem integral_sin_sq : ∫ x in a..b, sin x ^ 2 = (sin a * cos a - sin b * cos b + b - a) / 2 := by
  simp [field, integral_sin_pow, add_sub_assoc]

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