Theorems · Theorem · special functions

Polynomial.Chebyshev.abs_iterate_derivative_T_real_le

∀ (n : ℤ) (k : ℕ) {x : ℝ},
  |x| ≤ 1 →
    |Polynomial.eval x ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T ℝ n))| ≤
      Polynomial.eval 1 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T ℝ n))

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

Cites36

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

DFunLike.coestatement and proof · cited by 62,936
Realstatement and proof · cited by 25,697
RingHom.idstatement · cited by 18,349
LinearMapstatement · cited by 10,215
SetLike.coeproof · cited by 8,199
Polynomialstatement and proof · cited by 5,681
Set.imageproof · cited by 5,609
Finsuppproof · cited by 5,255
Finset.sumproof · cited by 5,195
mul_oneproof · cited by 3,885
Finset.sum_congrproof · cited by 2,323
le_reflproof · cited by 2,061

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.