Documentation

Mathlib.RingTheory.Polynomial.Chebyshev

Chebyshev polynomials #

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

Main definitions #

Main statements #

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] [ponton2020chebyshev]

TODO #

noncomputable def Polynomial.Chebyshev.T (R : Type u_1) [CommRing R] :

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

Equations
Instances For
    @[simp]
    theorem Polynomial.Chebyshev.T_one (R : Type u_1) [CommRing R] :
    Polynomial.Chebyshev.T R 1 = Polynomial.X
    @[simp]
    theorem Polynomial.Chebyshev.T_two (R : Type u_1) [CommRing R] :
    Polynomial.Chebyshev.T R 2 = 2 * Polynomial.X ^ 2 - 1
    theorem Polynomial.Chebyshev.T_of_two_le (R : Type u_1) [CommRing R] (n : ) (h : 2 n) :
    noncomputable def Polynomial.Chebyshev.U (R : Type u_1) [CommRing R] :

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

    Equations
    Instances For
      @[simp]
      theorem Polynomial.Chebyshev.U_one (R : Type u_1) [CommRing R] :
      Polynomial.Chebyshev.U R 1 = 2 * Polynomial.X
      @[simp]
      theorem Polynomial.Chebyshev.U_two (R : Type u_1) [CommRing R] :
      Polynomial.Chebyshev.U R 2 = 4 * Polynomial.X ^ 2 - 1
      theorem Polynomial.Chebyshev.U_of_two_le (R : Type u_1) [CommRing R] (n : ) (h : 2 n) :
      theorem Polynomial.Chebyshev.T_eq_X_mul_T_sub_pol_U (R : Type u_1) [CommRing R] (n : ) :
      Polynomial.Chebyshev.T R (n + 2) = Polynomial.X * Polynomial.Chebyshev.T R (n + 1) - (1 - Polynomial.X ^ 2) * Polynomial.Chebyshev.U R n
      @[simp]
      @[simp]
      theorem Polynomial.Chebyshev.T_derivative_eq_U {R : Type u_1} [CommRing R] (n : ) :
      Polynomial.derivative (Polynomial.Chebyshev.T R (n + 1)) = (n + 1) * Polynomial.Chebyshev.U R n
      theorem Polynomial.Chebyshev.one_sub_X_sq_mul_derivative_T_eq_poly_in_T {R : Type u_1} [CommRing R] (n : ) :
      (1 - Polynomial.X ^ 2) * Polynomial.derivative (Polynomial.Chebyshev.T R (n + 1)) = (n + 1) * (Polynomial.Chebyshev.T R n - Polynomial.X * Polynomial.Chebyshev.T R (n + 1))
      theorem Polynomial.Chebyshev.add_one_mul_T_eq_poly_in_U {R : Type u_1} [CommRing R] (n : ) :
      (n + 1) * Polynomial.Chebyshev.T R (n + 1) = Polynomial.X * Polynomial.Chebyshev.U R n - (1 - Polynomial.X ^ 2) * Polynomial.derivative (Polynomial.Chebyshev.U R n)

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

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