Documentation

Mathlib.RingTheory.Polynomial.Chebyshev

Chebyshev polynomials #

The Chebyshev polynomials are 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] [Pon20]

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
    theorem Polynomial.Chebyshev.induct (motive : Prop) (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]
    @[simp]
    theorem Polynomial.Chebyshev.T_one (R : Type u_1) [CommRing R] :
    Polynomial.Chebyshev.T R 1 = Polynomial.X
    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_neg_two (R : Type u_1) [CommRing R] :
    Polynomial.Chebyshev.T R (-2) = 2 * Polynomial.X ^ 2 - 1
    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]
      @[simp]
      theorem Polynomial.Chebyshev.U_one (R : Type u_1) [CommRing R] :
      Polynomial.Chebyshev.U R 1 = 2 * Polynomial.X
      theorem Polynomial.Chebyshev.U_two (R : Type u_1) [CommRing R] :
      Polynomial.Chebyshev.U R 2 = 4 * Polynomial.X ^ 2 - 1
      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) = 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} [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)

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

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