integral_sin_mul_sin_mul_cos_pow_eq

English

For hn ≥ 2 and hz ≠ 0, the sine-cosine power relation holds: ∫ sin(2 z x) sin x cos^n x dx = (n/(2 z)) ∫ cos(2 z x) cos^n x dx − (n-1)/(2 z) ∫ cos(2 z x) cos^{n-2} x dx.

Русский

Для n ≥ 2 и z ≠ 0 верна формула-отношение: ∫ sin(2 z x) sin x cos^n x dx = (n/(2 z)) ∫ cos(2 z x) cos^n x dx − (n-1)/(2 z) ∫ cos(2 z x) cos^{n-2} x dx.

LaTeX

$$$\int_{0}^{\frac{\pi}{2}} \sin(2 z x) \sin x \cos^{n} x \, dx = \frac{n}{2 z} \int_{0}^{\frac{\pi}{2}} \cos(2 z x) \cos^{n} x \, dx - \frac{n-1}{2 z} \int_{0}^{\frac{\pi}{2}} \cos(2 z x) \cos^{n-2} x \, dx$$$

Lean4

theorem integral_sin_mul_sin_mul_cos_pow_eq (hn : 2 ≤ n) (hz : z ≠ 0) :
    (∫ x in (0 : ℝ)..π / 2, Complex.sin (2 * z * x) * sin x * (cos x : ℂ) ^ (n - 1)) =
      (n / (2 * z) * ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ n) -
        (n - 1) / (2 * z) * ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (n - 2) :=
  by
  have der1 :
    ∀ x : ℝ,
      x ∈ uIcc 0 (π / 2) →
        HasDerivAt (fun y : ℝ => sin y * (cos y : ℂ) ^ (n - 1))
          ((cos x : ℂ) ^ n - (n - 1) * (sin x : ℂ) ^ 2 * (cos x : ℂ) ^ (n - 2)) x :=
    by
    intro x _
    have c := HasDerivAt.comp (x : ℂ) (hasDerivAt_pow (n - 1) _) (Complex.hasDerivAt_cos x)
    convert ((Complex.hasDerivAt_sin x).fun_mul c).comp_ofReal using 1
    · simp only [Complex.ofReal_sin, Complex.ofReal_cos, Function.comp]
    · simp only [Complex.ofReal_cos, Complex.ofReal_sin]
      rw [mul_neg, mul_neg, ← sub_eq_add_neg, Function.comp_apply]
      congr 1
      · rw [← pow_succ', Nat.sub_add_cancel (by cutsat : 1 ≤ n)]
      · have : ((n - 1 : ℕ) : ℂ) = (n : ℂ) - 1 := by rw [Nat.cast_sub (one_le_two.trans hn), Nat.cast_one]
        rw [Nat.sub_sub, this]
        ring
  convert integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_sin_comp_const_mul hz x) _ _ using 1
  · refine integral_congr fun x _ => ?_
    ring_nf
  · -- now a tedious rearrangement of terms
        -- gather into a single integral, and deal with continuity subgoals:

    rw [sin_zero, cos_pi_div_two, Complex.ofReal_zero, zero_pow, zero_mul, mul_zero, zero_mul, zero_mul, sub_zero,
      zero_sub, ← integral_neg, ← integral_const_mul, ← integral_const_mul, ← integral_sub]
    rotate_left
    · apply Continuous.intervalIntegrable
      exact
        continuous_const.mul
          ((Complex.continuous_cos.comp (continuous_const.mul Complex.continuous_ofReal)).mul
            ((Complex.continuous_ofReal.comp continuous_cos).pow n))
    · apply Continuous.intervalIntegrable
      exact
        continuous_const.mul
          ((Complex.continuous_cos.comp (continuous_const.mul Complex.continuous_ofReal)).mul
            ((Complex.continuous_ofReal.comp continuous_cos).pow (n - 2)))
    · exact Nat.sub_ne_zero_of_lt hn
    refine integral_congr fun x _ => ?_
    dsimp only
      -- get rid of real trig functions and divisions by 2 * z:

    rw [Complex.ofReal_cos, Complex.ofReal_sin, Complex.sin_sq, ← mul_div_right_comm, ← mul_div_right_comm, ← sub_div,
      mul_div, ← neg_div]
    congr 1
    have : Complex.cos x ^ n = Complex.cos x ^ (n - 2) * Complex.cos x ^ 2 := by
      conv_lhs => rw [← Nat.sub_add_cancel hn, pow_add]
    rw [this]
    ring
  · apply Continuous.intervalIntegrable
    exact
      ((Complex.continuous_ofReal.comp continuous_cos).pow n).sub
        ((continuous_const.mul ((Complex.continuous_ofReal.comp continuous_sin).pow 2)).mul
          ((Complex.continuous_ofReal.comp continuous_cos).pow (n - 2)))
  · apply Continuous.intervalIntegrable
    exact Complex.continuous_sin.comp (continuous_const.mul Complex.continuous_ofReal)

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