integral_sin_pow_odd — Mathlib

English

For natural m,n, the integral of sin^m x cos^{2n+1} x over [a,b] equals the integral over [cos b, cos a] of u^n (1−u^2)^m.

Русский

Для натуральных m,n интеграл sin^m x cos^{2n+1} x по [a,b] равен интегралу по [cos b, cos a] от u^n (1−u^2)^m.

LaTeX

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

Lean4

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

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