feat(analysis/special_functions/integrals): integral of `sin x ^ m * …

…cos x ^ n` (#7418)

The simplification of integrals of the form `∫ x in a..b, sin x ^ m * cos x ^ n` where (i) `n` is odd, (ii) `m` is odd, and (iii) `m` and `n` are both even.

The computation of the integrals of the following functions are then provided outright:
- `sin x * cos x`, given both in terms of sine and cosine
- `sin x ^ 2 * cos x ^ 2`
- `sin x ^ 2 * cos x` and `sin x * cos x ^ 2`
- `sin x ^ 3` and `cos x ^ 3`

src/analysis/special_functions/integrals.lean

@@ -15,6 +15,7 @@ This file contains proofs of the integrals of various specific functions. This i
 * Reduction formulae for the integrals of `sin x ^ n` and `cos x ^ n` for `n ≥ 2`
 * The computation of `∫ x in 0..π, sin x ^ n` as a product for even and odd `n` (used in proving the
   Wallis product for pi)
+* Integrals of the form `sin x ^ m * cos x ^ n`
 
 With these lemmas, many simple integrals can be computed by `simp` or `norm_num`.
 See `test/integration.lean` for specific examples.
@@ -286,8 +287,8 @@ begin
     λ x hx, by simpa only [neg_neg] using (has_deriv_at_cos x).neg,
   have H := integral_mul_deriv_eq_deriv_mul hu hv _ _,
   calc  ∫ x in a..b, sin x ^ (n + 2)
-      = ∫ x in a..b, sin x ^ (n + 1) * sin x : by simp only [pow_succ']
-  ... = C + (n + 1) * ∫ x in a..b, cos x ^ 2 * sin x ^ n : by simp [H, h, sq]
+      = ∫ x in a..b, sin x ^ (n + 1) * sin x                   : by simp only [pow_succ']
+  ... = C + (n + 1) * ∫ x in a..b, cos x ^ 2 * sin x ^ n       : by simp [H, h, sq]
   ... = C + (n + 1) * ∫ x in a..b, sin x ^ n - sin x ^ (n + 2) : by simp [cos_sq', sub_mul,
                                                                           ← pow_add, add_comm]
   ... = C + (n + 1) * (∫ x in a..b, sin x ^ n) - (n + 1) * ∫ x in a..b, sin x ^ (n + 2) :
@@ -341,8 +342,8 @@ lemma integral_sin_pow_antimono :
   ∫ x in 0..π, sin x ^ (n + 1) ≤ ∫ x in 0..π, sin x ^ n :=
 begin
   refine integral_mono_on _ _ pi_pos.le (λ x hx, _),
-  { exact ((continuous_pow (n + 1)).comp continuous_sin).interval_integrable 0 π },
-  { exact ((continuous_pow n).comp continuous_sin).interval_integrable 0 π },
+  { exact (continuous_sin.pow (n + 1)).interval_integrable 0 π },
+  { exact (continuous_sin.pow n).interval_integrable 0 π },
   { refine pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc _) (sin_le_one x) (nat.le_add_right n 1),
     rwa interval_of_le pi_pos.le at hx },
 end
@@ -360,8 +361,8 @@ begin
   have hv : ∀ x ∈ interval a b, has_deriv_at sin (cos x) x := λ x hx, has_deriv_at_sin x,
   have H := integral_mul_deriv_eq_deriv_mul hu hv _ _,
   calc  ∫ x in a..b, cos x ^ (n + 2)
-      = ∫ x in a..b, cos x ^ (n + 1) * cos x : by simp only [pow_succ']
-  ... = C + (n + 1) * ∫ x in a..b, sin x ^ 2 * cos x ^ n : by simp [H, h, sq, -neg_add_rev]
+      = ∫ x in a..b, cos x ^ (n + 1) * cos x                   : by simp only [pow_succ']
+  ... = C + (n + 1) * ∫ x in a..b, sin x ^ 2 * cos x ^ n       : by simp [H, h, sq, -neg_add_rev]
   ... = C + (n + 1) * ∫ x in a..b, cos x ^ n - cos x ^ (n + 2) : by simp [sin_sq, sub_mul,
                                                                           ← pow_add, add_comm]
   ... = C + (n + 1) * (∫ x in a..b, cos x ^ n) - (n + 1) * ∫ x in a..b, cos x ^ (n + 2) :
@@ -383,3 +384,80 @@ end
 @[simp]
 lemma integral_cos_sq : ∫ x in a..b, cos x ^ 2 = (cos b * sin b - cos a * sin a + b - a) / 2 :=
 by field_simp [integral_cos_pow, add_sub_assoc]
+
+/-! ### Integral of `sin x ^ m * cos x ^ n` -/
+
+/-- Simplification of the integral of `sin x ^ m * cos x ^ n`, case `n` is odd. -/
+lemma integral_sin_pow_mul_cos_pow_odd (m n : ℕ) :
+  ∫ x in a..b, sin x ^ m * cos x ^ (2 * n + 1) = ∫ u in sin a..sin b, u ^ m * (1 - u ^ 2) ^ n :=
+have hc : continuous (λ u : ℝ, u ^ m * (1 - u ^ 2) ^ n), by continuity,
+calc  ∫ x in a..b, sin x ^ m * cos x ^ (2 * n + 1)
+    = ∫ x in a..b, sin x ^ m * (1 - sin x ^ 2) ^ n * cos x : by simp only [pow_succ', ← mul_assoc,
+                                                                           pow_mul, cos_sq']
+... = ∫ u in sin a..sin b, u ^ m * (1 - u ^ 2) ^ n         : integral_comp_mul_deriv
+                                                              (λ x hx, has_deriv_at_sin x)
+                                                                continuous_on_cos hc
+
+/-- 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]
+lemma 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
+
+@[simp]
+lemma integral_sin_sq_mul_cos :
+  ∫ x in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3 :=
+by simpa using integral_sin_pow_mul_cos_pow_odd 2 0
+
+@[simp]
+lemma integral_cos_pow_three :
+  ∫ x in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3 :=
+by simpa using integral_sin_pow_mul_cos_pow_odd 0 1
+
+/-- Simplification of the integral of `sin x ^ m * cos x ^ n`, case `m` is odd. -/
+lemma integral_sin_pow_odd_mul_cos_pow (m n : ℕ) :
+  ∫ x in a..b, sin x ^ (2 * m + 1) * cos x ^ n = ∫ u in cos b..cos a, u ^ n * (1 - u ^ 2) ^ m :=
+have hc : continuous (λ u : ℝ, u ^ n * (1 - u ^ 2) ^ m), by continuity,
+calc   ∫ x in a..b, sin x ^ (2 * m + 1) * cos x ^ n
+    = -∫ x in b..a, sin x ^ (2 * m + 1) * cos x ^ n          : by rw integral_symm
+... =  ∫ x in b..a, (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n : by simp [pow_succ', pow_mul, sin_sq]
+... =  ∫ x in b..a, cos x ^ n * (1 - cos x ^ 2) ^ m * -sin x : by { congr, ext, ring }
+... =  ∫ u in cos b..cos a, u ^ n * (1 - u ^ 2) ^ m          : integral_comp_mul_deriv
+                                                                (λ x hx, has_deriv_at_cos x)
+                                                                  continuous_on_sin.neg hc
+
+/-- 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². -/
+lemma 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
+
+@[simp]
+lemma integral_sin_mul_cos_sq :
+  ∫ x in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3 :=
+by simpa using integral_sin_pow_odd_mul_cos_pow 0 2
+
+@[simp]
+lemma integral_sin_pow_three :
+  ∫ x in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3 :=
+by simpa using integral_sin_pow_odd_mul_cos_pow 1 0
+
+/-- Simplification of the integral of `sin x ^ m * cos x ^ n`, case `m` and `n` are both even. -/
+lemma integral_sin_pow_even_mul_cos_pow_even (m n : ℕ) :
+    ∫ x in a..b, sin x ^ (2 * m) * cos x ^ (2 * n)
+  = ∫ x in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n :=
+by field_simp [pow_mul, sin_sq, cos_sq, ← sub_sub, (by ring : (2:ℝ) - 1 = 1)]
+
+@[simp]
+lemma integral_sin_sq_mul_cos_sq :
+  ∫ x in a..b, sin x ^ 2 * cos x ^ 2 = (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 :=
+begin
+  convert integral_sin_pow_even_mul_cos_pow_even 1 1 using 1,
+  have h1 : ∀ c : ℝ, (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4 := λ c, by ring,
+  have h2 : continuous (λ x, cos (2 * x) ^ 2) := by continuity,
+  have h3 : ∀ x, cos x * sin x = sin (2 * x) / 2, { intro, rw sin_two_mul, ring },
+  have h4 : ∀ d : ℝ, 2 * (2 * d) = 4 * d := λ d, by ring,
+  simp [h1, h2.interval_integrable, integral_comp_mul_left (λ x, cos x ^ 2), h3, h4],
+  ring,
+end

test/integration.lean

@@ -29,10 +29,14 @@ example : ∫ x in 0..π, sin x = 2 := by norm_num
 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..1, 1 / (1 + x ^ 2) = π / 4 := by simp
 example : ∫ x in 0..2*π, sin x ^ 2 = π := by simp [mul_div_cancel_left]
-example : ∫ x in 0..π/2, cos x ^ 2 / 2 = π/8 := by norm_num [div_div_eq_div_mul]
+example : ∫ x in 0..π/2, cos x ^ 2 / 2 = π / 8 := by norm_num [div_div_eq_div_mul]
 example : ∫ x in 0..π, cos x ^ 2 - sin x ^ 2 = 0 := by simp [integral_cos_sq_sub_sin_sq]
+example : ∫ x in 0..π/2, sin x ^ 3 = 2 / 3 := by norm_num
+example : ∫ x in 0..π/2, cos x ^ 3 = 2 / 3 := by norm_num
+example : ∫ x in 0..π, sin x * cos x = 0 := by simp
+example : ∫ x in 0..π, sin x ^ 2 * cos x ^ 2 = π / 8 := by simpa using sin_nat_mul_pi 4
 
 /- the exponential function -/
 example : ∫ x in 0..2, -exp x = 1 - exp 2 := by simp
@@ -65,7 +69,7 @@ end
   difficult time recognizing the function you are trying to integrate -/
 example : ∫ x : ℝ in 0..2, 3 * (x + 1) ^ 2 = 26 :=
   by norm_num [integral_comp_add_right (λ x, x ^ 2)]
-example : ∫ x : ℝ in -1..0, (1 + (x + 1) ^ 2)⁻¹ = π/4 :=
+example : ∫ x : ℝ in -1..0, (1 + (x + 1) ^ 2)⁻¹ = π / 4 :=
   by simp [integral_comp_add_right (λ x, (1 + x ^ 2)⁻¹)]
 
 /-! ### Compositions of functions (aka "change of variables" or "integration by substitution") -/