Commit 2026-03-10 22:34 b7fcb007

View on Github →

feat(Chebyshev/RootsExtrema): bound iterated derivatives of Chebyshev T on [-1, 1] (#34364)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean

added theorem Polynomial.Chebyshev.abs_iterate_derivative_T_real_le

Modified Mathlib/RingTheory/Polynomial/Chebyshev.lean

added theorem Polynomial.Chebyshev.T_derivative_mem_span_T

added theorem Polynomial.Chebyshev.T_iterate_derivative_mem_span_T

added theorem Polynomial.Chebyshev.U_eq_two_mul_T_add_U

added theorem Polynomial.Chebyshev.U_mem_span_T

added theorem Polynomial.Chebyshev.two_mul_T_eq_U_sub_U