# Documentation

Mathlib.RingTheory.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.castRingHom R) interfering all the time.

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

## TODO #

• Redefine and/or relate the definition of Chebyshev polynomials to LinearRecurrence.
• 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.