English
For hn ≥ 2 and hz ≠ 0, the integral identity holds: ∫_0^{π/2} cos(2 z x) cos^n x dx = (n/(2 z)) ∫_0^{π/2} sin(2 z x) sin x cos^{n-1} x dx.
Русский
Для n ≥ 2 и z ≠ 0 верна идентичность: ∫_0^{π/2} cos(2 z x) cos^n x dx = (n/(2 z)) ∫_0^{π/2} sin(2 z x) sin x cos^{n-1} x dx.
LaTeX
$$$\int_{0}^{\frac{\pi}{2}} \cos(2 z x) \cos^{n} x \, dx = \frac{n}{2 z} \int_{0}^{\frac{\pi}{2}} \sin(2 z x) \sin x \cos^{n-1} x \, dx$$$
Lean4
theorem integral_cos_mul_cos_pow_aux (hn : 2 ≤ n) (hz : z ≠ 0) :
(∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ n) =
n / (2 * z) * ∫ x in (0 : ℝ)..π / 2, Complex.sin (2 * z * x) * sin x * (cos x : ℂ) ^ (n - 1) :=
by
have der1 :
∀ x : ℝ, x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y : ℝ => (cos y : ℂ) ^ n) (-n * sin x * (cos x : ℂ) ^ (n - 1)) x :=
by
intro x _
have b : HasDerivAt (fun y : ℝ => (cos y : ℂ)) (-sin x) x := by simpa using (hasDerivAt_cos x).ofReal_comp
convert HasDerivAt.comp x (hasDerivAt_pow _ _) b using 1
ring
convert (config := { sameFun := true })
integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_cos_comp_const_mul hz x) _ _ using 2
· ext1 x; rw [mul_comm]
· rw [Complex.ofReal_zero, mul_zero, Complex.sin_zero, zero_div, mul_zero, sub_zero, cos_pi_div_two,
Complex.ofReal_zero, zero_pow (by positivity : n ≠ 0), zero_mul, zero_sub, ← integral_neg, ← integral_const_mul]
refine integral_congr fun x _ => ?_
field_simp
· apply Continuous.intervalIntegrable
exact
(continuous_const.mul (Complex.continuous_ofReal.comp continuous_sin)).mul
((Complex.continuous_ofReal.comp continuous_cos).pow (n - 1))
· apply Continuous.intervalIntegrable
exact Complex.continuous_cos.comp (continuous_const.mul Complex.continuous_ofReal)
