Theorems · Theorem · special functions

Polynomial.Chebyshev.coeff_eq_iff_of_forall_abs_le_one

∀ {n : ℕ} {P : Polynomial ℝ},
  P.degree ≤ ↑n →
    (∀ x ∈ Set.Icc (-1) 1, |Polynomial.eval x P| ≤ 1) → (P.coeff n = 2 ^ (n - 1) ↔ P = Polynomial.Chebyshev.T ℝ ↑n)

Defined in: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Cited by: 1 results in Mathlib
Foundations: Depth 187 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.

Cites12

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

Setstatement · cited by 53,352
Realstatement and proof · cited by 25,697
Polynomialstatement and proof · cited by 5,681
absstatement and proof · cited by 1,814
Set.Iccstatement and proof · cited by 1,702
WithBotstatement · cited by 1,498
Polynomial.coeffstatement and proof · cited by 1,045
Polynomial.evalstatement and proof · cited by 796
Polynomial.degreestatement and proof · cited by 643
Polynomial.Chebyshev.Tstatement and proof · cited by 108
Polynomial.Chebyshev.sumNodesproof · cited by 6
Polynomial.Chebyshev.sumNodes_eq_sumNodes_T_iffproof · cited by 2

Cited by1

Results whose statement or proof uses this declaration.

Polynomial.Chebyshev.leadingCoeff_eq_iff_of_forall_abs_le_oneproof · cited by 0