Theorems · Theorem · special functions

Polynomial.Chebyshev.sumNodes_eq_sumNodes_T_iff

∀ {n : ℕ} {c : ℕ → ℝ},
  (∀ i ≤ n, 0 < (-1) ^ i * c i) →
    ∀ {P : Polynomial ℝ},
      P.degree ≤ ↑n →
        (∀ x ∈ Set.Icc (-1) 1, |Polynomial.eval x P| ≤ 1) →
          (Polynomial.Chebyshev.sumNodes n c P = Polynomial.Chebyshev.sumNodes n c (Polynomial.Chebyshev.T ℝ ↑n) ↔
            P = Polynomial.Chebyshev.T ℝ ↑n)

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

Cites40

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
Finset.sumproof · cited by 5,195
Finset.cardproof · cited by 2,327
Finset.sum_congrproof · cited by 2,323
le_reflproof · cited by 2,061
absstatement and proof · cited by 1,814
Set.Iccstatement and proof · cited by 1,702
WithBotstatement and proof · cited by 1,498
Finset.rangeproof · cited by 1,341
le_of_ltproof · cited by 1,175

Cited by2

Results whose statement or proof uses this declaration.

Polynomial.Chebyshev.coeff_eq_iff_of_forall_abs_le_oneproof · cited by 1
Polynomial.Chebyshev.eval_iterate_derivative_eq_iff_of_boundedproof · cited by 0