Theorems · Theorem · special functions

Polynomial.Chebyshev.integral_T_real_mul_self_measureT_of_ne_zero

∀ {n : ℕ},
  n ≠ 0 →
    ∫ (x : ℝ),
        Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) *
          Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) ∂Polynomial.Chebyshev.measureT =
      Real.pi / 2

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.

Cites11

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
zero_addproof · cited by 2,366
MeasureTheory.integralstatement and proof · cited by 1,779
Real.pistatement and proof · cited by 1,774
sub_selfproof · cited by 996
Polynomial.evalstatement and proof · cited by 796
Polynomial.Chebyshev.Tstatement and proof · cited by 108
Polynomial.Chebyshev.measureTstatement and proof · cited by 11
Polynomial.Chebyshev.integral_eval_T_real_measureT_of_ne_zeroproof · cited by 3
Polynomial.Chebyshev.integral_eval_T_real_measureT_zeroproof · cited by 3
Polynomial.Chebyshev.integral_eval_T_real_mul_eval_T_real_measureTproof · cited by 2

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.