# mathlibdocumentation

ring_theory.polynomial.chebyshev

# Chebyshev polynomials #

The Chebyshev polynomials are two families of polynomials indexed by ℕ, with integral coefficients.

## Main definitions #

• polynomial.chebyshev.T: the Chebyshev polynomials of the first kind.
• polynomial.chebyshev.U: the Chebyshev polynomials of the second kind.

## Main statements #

• The formal derivative of the Chebyshev polynomials of the first kind is a scalar multiple of the Chebyshev polynomials of the second kind.
• polynomial.chebyshev.mul_T, the product of the m-th and (m + k)-th Chebyshev polynomials of the first kind is the sum of the (2 * m + k)-th and k-th Chebyshev polynomials of the first kind.
• polynomial.chebyshev.T_mul, the (m * n)-th Chebyshev polynomial of the first kind is the composition of the m-th and n-th Chebyshev polynomials of the first kind.

## Implementation details #

Since Chebyshev polynomials have interesting behaviour over the complex numbers and modulo p, we define them to have coefficients in an arbitrary commutative ring, even though technically ℤ would suffice. The benefit of allowing arbitrary coefficient rings, is that the statements afterwards are clean, and do not have map (int.cast_ring_hom R) interfering all the time.

Lionel Ponton, Roots of the Chebyshev polynomials: A purely algebraic approach

## TODO #

• Redefine and/or relate the definition of Chebyshev polynomials to linear_recurrence.
• Add explicit formula involving square roots for Chebyshev polynomials
• Compute zeroes and extrema of Chebyshev polynomials.
• Prove that the roots of the Chebyshev polynomials (except 0) are irrational.
• Prove minimax properties of Chebyshev polynomials.