Theorems · Theorem · real analysis

integral_cos_pow

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

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

Defined in

Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Cited by

1 results in Mathlib

Foundations

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