Theorems · Theorem · real analysis

integral_sin_pow_mul_cos_pow_odd

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

Simplification of the integral of sin x ^ m * cos x ^ n, case n 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