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

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) [CommRing R] : ℤ → Polynomial R

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

Equations

• Polynomial.Chebyshev.T R 0 = 1
• Polynomial.Chebyshev.T R 1 = Polynomial.X
• Polynomial.Chebyshev.T R (Int.ofNat n.succ.succ) = 2 * Polynomial.X * Polynomial.Chebyshev.T R (↑n + 1) - Polynomial.Chebyshev.T R ↑n
• Polynomial.Chebyshev.T R (Int.negSucc n) = 2 * Polynomial.X * Polynomial.Chebyshev.T R (-↑n) - Polynomial.Chebyshev.T R (-↑n + 1)

theorem Polynomial.Chebyshev.induct (motive : ℤ → Prop) (zero : motive 0) (one : motive 1) (add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑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) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.T R (n + 2) = 2 * Polynomial.X * Polynomial.Chebyshev.T R (n + 1) - Polynomial.Chebyshev.T R n

theorem Polynomial.Chebyshev.T_add_one (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.T R (n + 1) = 2 * Polynomial.X * Polynomial.Chebyshev.T R n - Polynomial.Chebyshev.T R (n - 1)

theorem Polynomial.Chebyshev.T_sub_two (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.T R (n - 2) = 2 * Polynomial.X * Polynomial.Chebyshev.T R (n - 1) - Polynomial.Chebyshev.T R n

theorem Polynomial.Chebyshev.T_sub_one (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.T R (n - 1) = 2 * Polynomial.X * Polynomial.Chebyshev.T R n - Polynomial.Chebyshev.T R (n + 1)

theorem Polynomial.Chebyshev.T_eq (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.T R 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) [CommRing R] : Polynomial.Chebyshev.T R 0 = 1

@[simp]

theorem Polynomial.Chebyshev.T_one (R : Type u_1) [CommRing R] : Polynomial.Chebyshev.T R 1 = Polynomial.X

theorem Polynomial.Chebyshev.T_neg_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

@[simp]

theorem Polynomial.Chebyshev.T_neg (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.T R (-n) = Polynomial.Chebyshev.T R n

theorem Polynomial.Chebyshev.T_natAbs (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.T R ↑n.natAbs = Polynomial.Chebyshev.T R n

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] : ℤ → Polynomial R

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

Equations

• Polynomial.Chebyshev.U R 0 = 1
• Polynomial.Chebyshev.U R 1 = 2 * Polynomial.X
• Polynomial.Chebyshev.U R (Int.ofNat n.succ.succ) = 2 * Polynomial.X * Polynomial.Chebyshev.U R (↑n + 1) - Polynomial.Chebyshev.U R ↑n
• Polynomial.Chebyshev.U R (Int.negSucc n) = 2 * Polynomial.X * Polynomial.Chebyshev.U R (-↑n) - Polynomial.Chebyshev.U R (-↑n + 1)

@[simp]

theorem Polynomial.Chebyshev.U_add_two (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.U R (n + 2) = 2 * Polynomial.X * Polynomial.Chebyshev.U R (n + 1) - Polynomial.Chebyshev.U R n

theorem Polynomial.Chebyshev.U_add_one (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.U R (n + 1) = 2 * Polynomial.X * Polynomial.Chebyshev.U R n - Polynomial.Chebyshev.U R (n - 1)

theorem Polynomial.Chebyshev.U_sub_two (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.U R (n - 2) = 2 * Polynomial.X * Polynomial.Chebyshev.U R (n - 1) - Polynomial.Chebyshev.U R n

theorem Polynomial.Chebyshev.U_sub_one (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.U R (n - 1) = 2 * Polynomial.X * Polynomial.Chebyshev.U R n - Polynomial.Chebyshev.U R (n + 1)

theorem Polynomial.Chebyshev.U_eq (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.U R 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) [CommRing R] : Polynomial.Chebyshev.U R 0 = 1

@[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_neg_one (R : Type u_1) [CommRing R] : Polynomial.Chebyshev.U R (-1) = 0

theorem Polynomial.Chebyshev.U_two (R : Type u_1) [CommRing R] : Polynomial.Chebyshev.U R 2 = 4 * Polynomial.X ^ 2 - 1

@[simp]

theorem Polynomial.Chebyshev.U_neg_two (R : Type u_1) [CommRing R] : Polynomial.Chebyshev.U R (-2) = -1

theorem Polynomial.Chebyshev.U_neg_sub_one (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.U R (-n - 1) = -Polynomial.Chebyshev.U R (n - 1)

theorem Polynomial.Chebyshev.U_neg (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.U R (-n) = -Polynomial.Chebyshev.U R (n - 2)

@[simp]

theorem Polynomial.Chebyshev.U_neg_sub_two (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.U R (-n - 2) = -Polynomial.Chebyshev.U R n

theorem Polynomial.Chebyshev.U_eq_X_mul_U_add_T (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.U R (n + 1) = Polynomial.X * Polynomial.Chebyshev.U R n + Polynomial.Chebyshev.T R (n + 1)

theorem Polynomial.Chebyshev.T_eq_U_sub_X_mul_U (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.T R n = Polynomial.Chebyshev.U R n - Polynomial.X * Polynomial.Chebyshev.U R (n - 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

theorem Polynomial.Chebyshev.one_sub_X_sq_mul_U_eq_pol_in_T (R : Type u_1) [CommRing R] (n : ℤ) : (1 - Polynomial.X ^ 2) * Polynomial.Chebyshev.U R n = 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} [CommRing R] [CommRing S] (f : R →+* S) (n : ℤ) : Polynomial.map f (Polynomial.Chebyshev.T R n) = Polynomial.Chebyshev.T S n

@[simp]

theorem Polynomial.Chebyshev.map_U {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (n : ℤ) : Polynomial.map f (Polynomial.Chebyshev.U R n) = Polynomial.Chebyshev.U S n

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)

theorem Polynomial.Chebyshev.mul_T (R : Type u_1) [CommRing R] (m : ℤ) (k : ℤ) : 2 * Polynomial.Chebyshev.T R m * Polynomial.Chebyshev.T R k = Polynomial.Chebyshev.T R (m + k) + Polynomial.Chebyshev.T R (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) [CommRing R] (m : ℤ) (n : ℤ) : Polynomial.Chebyshev.T R (m * n) = (Polynomial.Chebyshev.T R m).comp (Polynomial.Chebyshev.T R n)

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