Theorems · Theorem · real analysis

integral_cos_pow_aux

∀ {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 + 1) * ∫ (x : ℝ) in a..b, Real.cos x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, Real.cos x ^ (n + 2)

Defined in

Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Cited by

1 results in Mathlib

Foundations

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