English
The integral of cos^{n+2} has a reduction formula with boundary terms and a pair of integral terms in cos^n.
Русский
Интеграл от cos^{n+2} удовлетворяет редукционной формуле с граничными членами и двумя интегралами cos^n.
LaTeX
$$$$\\displaystyle \\int_{a}^{b} \\cos^{(n+2)}x \\,dx = \\frac{\\cos b^{n+1}\\sin b - \\cos a^{n+1}\\sin a}{n+2} + \\frac{n+1}{n+2}\\int_{a}^{b} \\cos^{n}x \\,dx.$$$$
Lean4
theorem integral_cos_pow_aux :
(∫ x in a..b, cos x ^ (n + 2)) =
(cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + (n + 1) * ∫ x in a..b, cos x ^ n) -
(n + 1) * ∫ x in a..b, cos x ^ (n + 2) :=
by
let C := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
have h : ∀ α β γ : ℝ, β * α * γ * α = β * (α * α * γ) := fun α β γ => by ring
have hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => cos y ^ (n + 1)) (-(n + 1 : ℕ) * sin x * cos x ^ n) x := fun x _ => by
simpa only [mul_right_comm, neg_mul, mul_neg] using (hasDerivAt_cos x).pow (n + 1)
have hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x := fun x _ => hasDerivAt_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 [_root_.pow_succ]
_ = C + (n + 1) * ∫ x in a..b, sin x ^ 2 * cos x ^ n := by simp [C, 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) := by
rw [integral_sub, mul_sub, add_sub_assoc] <;> apply Continuous.intervalIntegrable <;> fun_prop
all_goals apply Continuous.intervalIntegrable; fun_prop
