integral_sin_pow_even_mul_cos_pow_even

English

If both exponents are even, sin^m x cos^n x integral transforms to a product of halves: ((1 - cos 2x)/2)^m ((1+cos 2x)/2)^n, integrated over [a,b].

Русский

Если оба показателя чётны, интеграл sin^m x cos^n x переводится в произведение полов: ((1 - cos 2x)/2)^m ((1+cos 2x)/2)^n, по [a,b].

LaTeX

$$$$\\int_{a}^{b} \\sin^{2m}x \\cos^{2n}x \\,dx = \\int_{a}^{b} \\left(\\frac{1-\\cos(2x)}{2}\\right)^{m} \\left(\\frac{1+\\cos(2x)}{2}\\right)^{n} dx.$$$$

Lean4

/-- Simplification of the integral of `sin x ^ m * cos x ^ n`, case `m` and `n` are both even. -/
theorem integral_sin_pow_even_mul_cos_pow_even (m n : ℕ) :
    (∫ x in a..b, sin x ^ (2 * m) * cos x ^ (2 * n)) =
      ∫ x in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n :=
  by
  simp [pow_mul, sin_sq, cos_sq, ← sub_sub]
  field_simp
  norm_num

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