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.

References #

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.
def polynomial.chebyshev.T (R : Type u_1) [comm_ring R] :

T n is the n-th Chebyshev polynomial of the first kind

Equations
@[simp]
theorem polynomial.chebyshev.T_zero (R : Type u_1) [comm_ring R] :
@[simp]
theorem polynomial.chebyshev.T_one (R : Type u_1) [comm_ring R] :
theorem polynomial.chebyshev.T_two (R : Type u_1) [comm_ring R] :
= 2 * - 1
@[simp]
theorem polynomial.chebyshev.T_add_two (R : Type u_1) [comm_ring R] (n : ) :
(n + 2) = * (n + 1) -
theorem polynomial.chebyshev.T_of_two_le (R : Type u_1) [comm_ring R] (n : ) (h : 2 n) :
= * (n - 1) - (n - 2)
theorem polynomial.chebyshev.map_T {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (f : R →+* S) (n : ) :
def polynomial.chebyshev.U (R : Type u_1) [comm_ring R] :

U n is the n-th Chebyshev polynomial of the second kind

Equations
@[simp]
theorem polynomial.chebyshev.U_zero (R : Type u_1) [comm_ring R] :
@[simp]
theorem polynomial.chebyshev.U_one (R : Type u_1) [comm_ring R] :
theorem polynomial.chebyshev.U_two (R : Type u_1) [comm_ring R] :
= 4 * - 1
@[simp]
theorem polynomial.chebyshev.U_add_two (R : Type u_1) [comm_ring R] (n : ) :
(n + 2) = * (n + 1) -
theorem polynomial.chebyshev.U_of_two_le (R : Type u_1) [comm_ring R] (n : ) (h : 2 n) :
= * (n - 1) - (n - 2)
theorem polynomial.chebyshev.U_eq_X_mul_U_add_T (R : Type u_1) [comm_ring R] (n : ) :
(n + 1) = + (n + 1)
theorem polynomial.chebyshev.T_eq_U_sub_X_mul_U (R : Type u_1) [comm_ring R] (n : ) :
(n + 1) = (n + 1) -
theorem polynomial.chebyshev.T_eq_X_mul_T_sub_pol_U (R : Type u_1) [comm_ring R] (n : ) :
(n + 2) = polynomial.X * (n + 1) - (1 - *
theorem polynomial.chebyshev.one_sub_X_sq_mul_U_eq_pol_in_T (R : Type u_1) [comm_ring R] (n : ) :
(1 - * = polynomial.X * (n + 1) - (n + 2)
@[simp]
theorem polynomial.chebyshev.map_U {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (f : R →+* S) (n : ) :
theorem polynomial.chebyshev.T_derivative_eq_U {R : Type u_1} [comm_ring R] (n : ) :
= (n + 1) *
theorem polynomial.chebyshev.add_one_mul_T_eq_poly_in_U {R : Type u_1} [comm_ring R] (n : ) :
(n + 1) * (n + 1) =
theorem polynomial.chebyshev.mul_T (R : Type u_1) [comm_ring R] (m k : ) :
(2 * * (m + k) = (2 * m + k) +

The product of two Chebyshev polynomials is the sum of two other Chebyshev polynomials.

theorem polynomial.chebyshev.T_mul (R : Type u_1) [comm_ring R] (m n : ) :
(m * n) = .comp

The (m * n)-th Chebyshev polynomial is the composition of the m-th and n-th