Theorems · Theorem · special functions

EulerSine.integral_sin_mul_sin_mul_cos_pow_eq

∀ {z : ℂ} {n : ℕ},
  2 ≤ n →
    z ≠ 0 →
      ∫ (x : ℝ) in 0..Real.pi / 2, Complex.sin (2 * z * ↑x) * ↑(Real.sin x) * ↑(Real.cos x) ^ (n - 1) =
        (↑n / (2 * z) * ∫ (x : ℝ) in 0..Real.pi / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ n) -
          (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0..Real.pi / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ (n - 2)

Defined in: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Cited by: 1 results in Mathlib
Foundations: Depth 272 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites68

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
TopologicalSpaceproof · cited by 24,529
Moduleproof · cited by 20,661
AddCommGroupproof · cited by 12,871
NontriviallyNormedFieldproof · cited by 8,742
Complexstatement and proof · cited by 5,565
mul_oneproof · cited by 3,885
LE.le.transproof · cited by 3,151
add_zeroproof · cited by 2,707
Nat.cast_oneproof · cited by 2,501
MulZeroClass.mul_zeroproof · cited by 2,091
Real.pistatement and proof · cited by 1,774

Cited by1

Results whose statement or proof uses this declaration.

EulerSine.integral_cos_mul_cos_powproof · cited by 1