integral_sin_pow_even — Mathlib

English

For natural m,n, the integral of sin^m x cos^n x with n odd can be reduced to an integral over a transformed variable.

Русский

Для натуральных m,n интеграл sin^m x cos^n x при нечетном n может быть сведен к интегралу по преобразованной переменной.

LaTeX

$$$$\\displaystyle \\int_{a}^{b} \\sin^{m}x \\cos^{n}x \\;dx = \\int_{\\cos b}^{\\cos a} u^{n} (1-u^{2})^{m} \\;du \\quad (n=2k+1).$$$$

Lean4

theorem integral_sin_pow_even : (∫ x in 0..π, sin x ^ (2 * n)) = π * ∏ i ∈ range n, (2 * (i : ℝ) + 1) / (2 * i + 2) :=
  by
  induction n with
  | zero => simp
  | succ k ih =>
    rw [prod_range_succ_comm, mul_left_comm, ← ih, mul_succ, integral_sin_pow]
    norm_cast
    field_simp
    simp

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