Theorems · Theorem · real analysis

integral_sin_pow

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

The reduction formula for the integral of sin x ^ n for any natural n ≥ 2.

Defined in

Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Cited by

5 results in Mathlib

Foundations

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