English
For t real, the integral of sin(x)^{n+2} over [a,b] equals a boundary term plus (n+1) times the integral of sin(x)^n over [a,b] minus (n+1) times the integral of sin(x)^{n+2} over [a,b].
Русский
Для действительного n интеграл от a до b sin(x)^{n+2}dx равен константному приращению на границах плюс (n+1) умножить на интеграл sin(x)^n dx минус (n+1) умножить на интеграл sin(x)^{n+2} dx.
LaTeX
$$$$\\displaystyle \\int_{a}^{b} \\sin^{(n+2)}x \,dx = \\big( \\sin a^{n+1} \\cos a - \\sin b^{n+1} \\cos b \\big) + (n+1)\\int_{a}^{b} \\sin^{n}x\\,dx - (n+1)\\int_{a}^{b} \\sin^{n+2}x\\,dx.$$$$
Lean4
theorem integral_sin_pow_aux :
(∫ x in a..b, sin x ^ (n + 2)) =
(sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ x in a..b, sin x ^ n) -
(↑n + 1) * ∫ x in a..b, sin x ^ (n + 2) :=
by
let C := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
have h : ∀ α β γ : ℝ, β * α * γ * α = β * (α * α * γ) := fun α β γ => by ring
have hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => sin y ^ (n + 1)) ((n + 1 : ℕ) * cos x * sin x ^ n) x := fun x _ => by
simpa only [mul_right_comm] using (hasDerivAt_sin x).pow (n + 1)
have hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x := fun x _ => by
simpa only [neg_neg] using (hasDerivAt_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 [_root_.pow_succ]
_ = C + (↑n + 1) * ∫ x in a..b, cos x ^ 2 * sin x ^ n := by simp [H, h, sq]; ring
_ = 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) := by
rw [integral_sub, mul_sub, add_sub_assoc] <;> apply Continuous.intervalIntegrable <;> fun_prop
all_goals apply Continuous.intervalIntegrable; fun_prop
