Theorems · Theorem · special functions

Polynomial.Chebyshev.integral_eval_T_real_mul_self_measureT_zero

∫ (x : ℝ),
    Polynomial.eval x (Polynomial.Chebyshev.T ℝ 0) *
      Polynomial.eval x (Polynomial.Chebyshev.T ℝ 0) ∂Polynomial.Chebyshev.measureT =
  Real.pi

Defined in: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Cited by: 0 results in Mathlib
Foundations: Depth 286 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.

Cites9

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
mul_oneproof · cited by 3,885
MeasureTheory.integralstatement and proof · cited by 1,779
Real.pistatement and proof · cited by 1,774
Polynomial.evalstatement and proof · cited by 796
Polynomial.Chebyshev.Tstatement and proof · cited by 108
Polynomial.Chebyshev.T_zeroproof · cited by 21
Polynomial.Chebyshev.measureTstatement and proof · cited by 11
Polynomial.Chebyshev.integral_eval_T_real_measureT_zeroproof · cited by 3

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.