Theorems · Theorem · special functions
EulerSine.sin_pi_mul_eq
∀ (z : ℂ) (n : ℕ),
Complex.sin (↑Real.pi * z) =
((↑Real.pi * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
∫ (x : ℝ) in 0..Real.pi / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ (2 * n)) /
↑(∫ (x : ℝ) in 0..Real.pi / 2, Real.cos x ^ (2 * n))Finite form of Euler's sine product, with remainder term expressed as a ratio of cosine integrals.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 277 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites59
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
- NormedAddCommGroupproof · cited by 15,752
- NormedSpaceproof · cited by 12,499
- MeasureTheory.Measureproof · cited by 10,939
- Complexstatement and proof · cited by 5,565
- mul_oneproof · cited by 3,885
- one_mulproof · cited by 2,841
- zero_addproof · cited by 2,366
- Finset.prodstatement and proof · cited by 2,356
- mul_commproof · cited by 2,262
- MulZeroClass.mul_zeroproof · cited by 2,091
- Nat.cast_zeroproof · cited by 1,870
Cited by1
Results whose statement or proof uses this declaration.
- Complex.tendsto_euler_sin_prodproof · cited by 3