Theorems · Theorem · real analysis

integral_sin_pow_odd_mul_cos_pow

∀ {a b : ℝ} (m n : ℕ),
  ∫ (x : ℝ) in a..b, Real.sin x ^ (2 * m + 1) * Real.cos x ^ n =
    ∫ (u : ℝ) in Real.cos b..Real.cos a, u ^ n * (1 - u ^ 2) ^ m

Simplification of the integral of sin x ^ m * cos x ^ n, case m is odd.

Defined in

Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Cited by

3 results in Mathlib

Foundations

Depth 272 from the axioms · uses propext, Classical.choice, Quot.sound