# Chebyshev polynomials #

The Chebyshev polynomials are 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, twice the product of the m-th and k-th Chebyshev polynomials of the first kind is the sum of the m + k-th and m - 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.

## References #

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

## 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.
noncomputable def Polynomial.Chebyshev.T (R : Type u_1) [] :

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

Equations
Instances For
theorem Polynomial.Chebyshev.induct (motive : ) (zero : motive 0) (one : motive 1) (add_two : ∀ (n : ), motive (n + 1)motive nmotive (n + 2)) (neg_add_one : ∀ (n : ), motive (-n)motive (-n + 1)motive (-n - 1)) (a : ) :
motive a

Induction principle used for proving facts about Chebyshev polynomials.

@[simp]
theorem Polynomial.Chebyshev.T_add_two (R : Type u_1) [] (n : ) :
Polynomial.Chebyshev.T R (n + 2) = 2 * Polynomial.X * Polynomial.Chebyshev.T R (n + 1) -
theorem Polynomial.Chebyshev.T_add_one (R : Type u_1) [] (n : ) :
Polynomial.Chebyshev.T R (n + 1) = 2 * Polynomial.X * - Polynomial.Chebyshev.T R (n - 1)
theorem Polynomial.Chebyshev.T_sub_two (R : Type u_1) [] (n : ) :
Polynomial.Chebyshev.T R (n - 2) = 2 * Polynomial.X * Polynomial.Chebyshev.T R (n - 1) -
theorem Polynomial.Chebyshev.T_sub_one (R : Type u_1) [] (n : ) :
Polynomial.Chebyshev.T R (n - 1) = 2 * Polynomial.X * - Polynomial.Chebyshev.T R (n + 1)
theorem Polynomial.Chebyshev.T_eq (R : Type u_1) [] (n : ) :
= 2 * Polynomial.X * Polynomial.Chebyshev.T R (n - 1) - Polynomial.Chebyshev.T R (n - 2)
@[simp]
theorem Polynomial.Chebyshev.T_zero (R : Type u_1) [] :
@[simp]
theorem Polynomial.Chebyshev.T_one (R : Type u_1) [] :
= Polynomial.X
theorem Polynomial.Chebyshev.T_neg_one (R : Type u_1) [] :
= Polynomial.X
theorem Polynomial.Chebyshev.T_two (R : Type u_1) [] :
= 2 * Polynomial.X ^ 2 - 1
@[simp]
theorem Polynomial.Chebyshev.T_neg (R : Type u_1) [] (n : ) :
theorem Polynomial.Chebyshev.T_natAbs (R : Type u_1) [] (n : ) :
Polynomial.Chebyshev.T R n.natAbs =
theorem Polynomial.Chebyshev.T_neg_two (R : Type u_1) [] :
= 2 * Polynomial.X ^ 2 - 1
noncomputable def Polynomial.Chebyshev.U (R : Type u_1) [] :

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

Equations
Instances For
@[simp]
theorem Polynomial.Chebyshev.U_add_two (R : Type u_1) [] (n : ) :
Polynomial.Chebyshev.U R (n + 2) = 2 * Polynomial.X * Polynomial.Chebyshev.U R (n + 1) -
theorem Polynomial.Chebyshev.U_add_one (R : Type u_1) [] (n : ) :
Polynomial.Chebyshev.U R (n + 1) = 2 * Polynomial.X * - Polynomial.Chebyshev.U R (n - 1)
theorem Polynomial.Chebyshev.U_sub_two (R : Type u_1) [] (n : ) :
Polynomial.Chebyshev.U R (n - 2) = 2 * Polynomial.X * Polynomial.Chebyshev.U R (n - 1) -
theorem Polynomial.Chebyshev.U_sub_one (R : Type u_1) [] (n : ) :
Polynomial.Chebyshev.U R (n - 1) = 2 * Polynomial.X * - Polynomial.Chebyshev.U R (n + 1)
theorem Polynomial.Chebyshev.U_eq (R : Type u_1) [] (n : ) :
= 2 * Polynomial.X * Polynomial.Chebyshev.U R (n - 1) - Polynomial.Chebyshev.U R (n - 2)
@[simp]
theorem Polynomial.Chebyshev.U_zero (R : Type u_1) [] :
@[simp]
theorem Polynomial.Chebyshev.U_one (R : Type u_1) [] :
= 2 * Polynomial.X
@[simp]
theorem Polynomial.Chebyshev.U_neg_one (R : Type u_1) [] :
= 0
theorem Polynomial.Chebyshev.U_two (R : Type u_1) [] :
= 4 * Polynomial.X ^ 2 - 1
@[simp]
theorem Polynomial.Chebyshev.U_neg_two (R : Type u_1) [] :
= -1
@[simp]
theorem Polynomial.Chebyshev.T_eq_U_sub_X_mul_U (R : Type u_1) [] (n : ) :
= - Polynomial.X * Polynomial.Chebyshev.U R (n - 1)
theorem Polynomial.Chebyshev.T_eq_X_mul_T_sub_pol_U (R : Type u_1) [] (n : ) :
Polynomial.Chebyshev.T R (n + 2) = Polynomial.X * Polynomial.Chebyshev.T R (n + 1) - (1 - Polynomial.X ^ 2) *
theorem Polynomial.Chebyshev.one_sub_X_sq_mul_U_eq_pol_in_T (R : Type u_1) [] (n : ) :
(1 - Polynomial.X ^ 2) * = Polynomial.X * Polynomial.Chebyshev.T R (n + 1) - Polynomial.Chebyshev.T R (n + 2)
@[simp]
theorem Polynomial.Chebyshev.map_T {R : Type u_1} {S : Type u_2} [] [] (f : R →+* S) (n : ) :
@[simp]
theorem Polynomial.Chebyshev.map_U {R : Type u_1} {S : Type u_2} [] [] (f : R →+* S) (n : ) :
theorem Polynomial.Chebyshev.T_derivative_eq_U {R : Type u_1} [] (n : ) :
Polynomial.derivative () = n * Polynomial.Chebyshev.U R (n - 1)
theorem Polynomial.Chebyshev.one_sub_X_sq_mul_derivative_T_eq_poly_in_T {R : Type u_1} [] (n : ) :
(1 - Polynomial.X ^ 2) * Polynomial.derivative (Polynomial.Chebyshev.T R (n + 1)) = (n + 1) * ( - Polynomial.X * Polynomial.Chebyshev.T R (n + 1))
theorem Polynomial.Chebyshev.add_one_mul_T_eq_poly_in_U {R : Type u_1} [] (n : ) :
(n + 1) * Polynomial.Chebyshev.T R (n + 1) = Polynomial.X * - (1 - Polynomial.X ^ 2) * Polynomial.derivative ()
theorem Polynomial.Chebyshev.mul_T (R : Type u_1) [] (m : ) (k : ) :

Twice the product of two Chebyshev T polynomials is the sum of two other Chebyshev T polynomials.

theorem Polynomial.Chebyshev.T_mul (R : Type u_1) [] (m : ) (n : ) :
Polynomial.Chebyshev.T R (m * n) = ().comp ()

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