integral_cos_sq_sub_sin_sq — Mathlib

English

For real a,b, ∫_a^b (cos^2 x − sin^2 x) dx equals sin b cos b − sin a cos a.

Русский

Для действительных a,b интеграл от (cos^2 x − sin^2 x) по [a,b] равен sin b cos b − sin a cos a.

LaTeX

$$$\forall a,b \in \mathbb{R},\ \displaystyle \int_a^b (\cos^2 x - \sin^2 x) \, dx = \sin b \cos b - \sin a \cos a$$$

Lean4

theorem integral_cos_sq_sub_sin_sq : ∫ x in a..b, cos x ^ 2 - sin x ^ 2 = sin b * cos b - sin a * cos a := by
  simpa only [sq, sub_eq_add_neg, neg_mul_eq_mul_neg] using
    integral_deriv_mul_eq_sub (fun x _ => hasDerivAt_sin x) (fun x _ => hasDerivAt_cos x)
      continuousOn_cos.intervalIntegrable continuousOn_sin.neg.intervalIntegrable

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