feat(analysis/special_functions/integrals): integral of `cos x ^ 2 - …

…sin x ^ 2` (#7012)

An example of a direct application of integration by parts.

src/analysis/special_functions/integrals.lean

@@ -14,6 +14,7 @@ This file contains proofs of the integrals of various simple functions, includin
 There are also facts about more complicated integrals:
 * `sin x ^ n`: We prove a recursive formula for `sin x ^ (n + 2)` in terms of `sin x ^ n`,
   along with explicit product formulas for even and odd `n`.
+* `cos x ^ 2 - sin x ^ 2`
 
 With these lemmas, many simple integrals can be computed by `simp` or `norm_num`.
 See `test/integration.lean` for specific examples.
@@ -222,6 +223,11 @@ end
 lemma integral_cos : ∫ x in a..b, cos x = sin b - sin a :=
 by rw integral_deriv_eq_sub'; norm_num [continuous_on_cos]
 
+lemma 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 [pow_two, sub_eq_add_neg, neg_mul_eq_mul_neg] using integral_deriv_mul_eq_sub
+  (λ x hx, has_deriv_at_sin x) (λ x hx, has_deriv_at_cos x) continuous_on_cos continuous_on_sin.neg
+
 @[simp]
 lemma integral_inv_one_add_sq : ∫ x : ℝ in a..b, (1 + x^2)⁻¹ = arctan b - arctan a :=
 begin

test/integration.lean

@@ -28,6 +28,7 @@ example : ∫ x in 0..π/4, cos x = sqrt 2 / 2 := by simp
 example : ∫ x in 0..π, 2 * sin x = 4 := by norm_num
 example : ∫ x in 0..π/2, cos x / 2 = 1 / 2 := by simp
 example : ∫ x : ℝ in 0..1, 1 / (1 + x ^ 2) = π/4 := by simp
+example : ∫ x in 0..π, cos x ^ 2 - sin x ^ 2 = 0 := by simp [integral_cos_sq_sub_sin_sq]
 
 /-- the exponential function -/
 example : ∫ x in 0..2, -exp x = 1 - exp 2 := by simp