Theorem Polynomial.Chebyshev.abs_iterate_derivative_T_real_le

Modification history

2026-03-10 22:34
Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean
feat(Chebyshev/RootsExtrema): bound iterated derivatives of Chebyshev T on [-1, 1] (#34364)
Added Polynomial.Chebyshev.abs_iterate_derivative_T_real_leView on Github →