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 + 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.
(m * n)-th Chebyshev polynomial of the first kind is the composition of the
n-th Chebyshev polynomials of the first kind.
Implementation details #
Since Chebyshev polynomials have interesting behaviour over the complex numbers and modulo
we define them to have coefficients in an arbitrary commutative ring, even though
ℤ 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
- Redefine and/or relate the definition of Chebyshev polynomials to
- 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.
T n is the
n-th Chebyshev polynomial of the first kind
- polynomial.chebyshev.T R (n + 2) = 2 * polynomial.X * polynomial.chebyshev.T R n.succ - polynomial.chebyshev.T R n
- polynomial.chebyshev.T R 1 = polynomial.X
- polynomial.chebyshev.T R 0 = 1
U n is the
n-th Chebyshev polynomial of the second kind
- polynomial.chebyshev.U R (n + 2) = 2 * polynomial.X * polynomial.chebyshev.U R n.succ - polynomial.chebyshev.U R n
- polynomial.chebyshev.U R 1 = 2 * polynomial.X
- polynomial.chebyshev.U R 0 = 1
The product of two Chebyshev polynomials is the sum of two other Chebyshev polynomials.
(m * n)-th Chebyshev polynomial is the composition of the