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.
• Polynomial.Chebyshev.C: the rescaled Chebyshev polynomials of the first kind (also known as the Vieta–Lucas polynomials), given by $C_n(2x) = 2T_n(x)$.
• Polynomial.Chebyshev.S: the rescaled Chebyshev polynomials of the second kind (also known as the Vieta–Fibonacci polynomials), given by $S_n(2x) = U_n(x)$.

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.T_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. There is a similar statement Polynomial.Chebyshev.C_mul_C for the C polynomials.
• 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. There is a similar statement Polynomial.Chebyshev.C_mul for the C polynomials.

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.

@[irreducible]

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 : ℤ) : T R (n + 2) = 2 * X * T R (n + 1) - T R n

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

@[simp]

theorem Polynomial.Chebyshev.T_eval_one (R : Type u_1) [CommRing R] (n : ℤ) : eval 1 (T R n) = 1

@[simp]

theorem Polynomial.Chebyshev.T_eval_neg_one (R : Type u_1) [CommRing R] (n : ℤ) : eval (-1) (T R n) = ↑↑n.negOnePow

@[irreducible]

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 : ℤ) : U R (n + 2) = 2 * X * U R (n + 1) - U R n

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

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

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

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

@[simp]

theorem Polynomial.Chebyshev.U_zero (R : Type u_1) [CommRing R] : U R 0 = 1

@[simp]

theorem Polynomial.Chebyshev.U_one (R : Type u_1) [CommRing R] : U R 1 = 2 * X

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

theorem Polynomial.Chebyshev.U_eval_one (R : Type u_1) [CommRing R] (n : ℤ) : eval 1 (U R n) = ↑n + 1

@[simp]

theorem Polynomial.Chebyshev.U_eval_neg_one (R : Type u_1) [CommRing R] (n : ℤ) : eval (-1) (U R n) = ↑↑n.negOnePow * (↑n + 1)

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

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

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

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

@[irreducible]

noncomputable def Polynomial.Chebyshev.C (R : Type u_1) [CommRing R] : ℤ → Polynomial R

C n is the nth rescaled Chebyshev polynomial of the first kind (also known as a Vieta–Lucas polynomial), given by $C_n(2x) = 2T_n(x)$. See Polynomial.Chebyshev.C_comp_two_mul_X.

Equations

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

@[simp]

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

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

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

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

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

@[simp]

theorem Polynomial.Chebyshev.C_zero (R : Type u_1) [CommRing R] : C R 0 = 2

@[simp]

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

theorem Polynomial.Chebyshev.C_neg_one (R : Type u_1) [CommRing R] : C R (-1) = X

theorem Polynomial.Chebyshev.C_two (R : Type u_1) [CommRing R] : C R 2 = X ^ 2 - 2

@[simp]

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

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

theorem Polynomial.Chebyshev.C_neg_two (R : Type u_1) [CommRing R] : C R (-2) = X ^ 2 - 2

theorem Polynomial.Chebyshev.C_comp_two_mul_X (R : Type u_1) [CommRing R] (n : ℤ) : (C R n).comp (2 * X) = 2 * T R n

@[simp]

theorem Polynomial.Chebyshev.C_eval_two (R : Type u_1) [CommRing R] (n : ℤ) : eval 2 (C R n) = 2

@[simp]

theorem Polynomial.Chebyshev.C_eval_neg_two (R : Type u_1) [CommRing R] (n : ℤ) : eval (-2) (C R n) = 2 * ↑↑n.negOnePow

theorem Polynomial.Chebyshev.C_eq_two_mul_T_comp_half_mul_X (R : Type u_1) [CommRing R] [Invertible 2] (n : ℤ) : C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X)

theorem Polynomial.Chebyshev.T_eq_half_mul_C_comp_two_mul_X (R : Type u_1) [CommRing R] [Invertible 2] (n : ℤ) : T R n = Polynomial.C ⅟2 * (C R n).comp (2 * X)

@[irreducible]

noncomputable def Polynomial.Chebyshev.S (R : Type u_1) [CommRing R] : ℤ → Polynomial R

S n is the nth rescaled Chebyshev polynomial of the second kind (also known as a Vieta–Fibonacci polynomial), given by $S_n(2x) = U_n(x)$. See Polynomial.Chebyshev.S_comp_two_mul_X.

Equations

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

@[simp]

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

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

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

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

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

@[simp]

theorem Polynomial.Chebyshev.S_zero (R : Type u_1) [CommRing R] : S R 0 = 1

@[simp]

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

@[simp]

theorem Polynomial.Chebyshev.S_neg_one (R : Type u_1) [CommRing R] : S R (-1) = 0

theorem Polynomial.Chebyshev.S_two (R : Type u_1) [CommRing R] : S R 2 = X ^ 2 - 1

@[simp]

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

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

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

@[simp]

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

@[simp]

theorem Polynomial.Chebyshev.S_eval_two (R : Type u_1) [CommRing R] (n : ℤ) : eval 2 (S R n) = ↑n + 1

@[simp]

theorem Polynomial.Chebyshev.S_eval_neg_two (R : Type u_1) [CommRing R] (n : ℤ) : eval (-2) (S R n) = ↑↑n.negOnePow * (↑n + 1)

theorem Polynomial.Chebyshev.S_comp_two_mul_X (R : Type u_1) [CommRing R] (n : ℤ) : (S R n).comp (2 * X) = U R n

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

theorem Polynomial.Chebyshev.S_eq_U_comp_half_mul_X (R : Type u_1) [CommRing R] [Invertible 2] (n : ℤ) : S R n = (U R n).comp (Polynomial.C ⅟2 * X)

theorem Polynomial.Chebyshev.S_eq_X_mul_S_add_C (R : Type u_1) [CommRing R] (n : ℤ) : 2 * S R (n + 1) = X * S R n + C R (n + 1)

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Polynomial.Chebyshev.aeval_T {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [Algebra R R'] (x : R') (n : ℤ) : (aeval x) (T R n) = eval x (T R' n)

@[simp]

theorem Polynomial.Chebyshev.aeval_U {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [Algebra R R'] (x : R') (n : ℤ) : (aeval x) (U R n) = eval x (U R' n)

@[simp]

theorem Polynomial.Chebyshev.aeval_C {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [Algebra R R'] (x : R') (n : ℤ) : (aeval x) (C R n) = eval x (C R' n)

@[simp]

theorem Polynomial.Chebyshev.aeval_S {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [Algebra R R'] (x : R') (n : ℤ) : (aeval x) (S R n) = eval x (S R' n)

@[simp]

theorem Polynomial.Chebyshev.algebraMap_eval_T {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [Algebra R R'] (x : R) (n : ℤ) : (algebraMap R R') (eval x (T R n)) = eval ((algebraMap R R') x) (T R' n)

@[simp]

theorem Polynomial.Chebyshev.algebraMap_eval_U {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [Algebra R R'] (x : R) (n : ℤ) : (algebraMap R R') (eval x (U R n)) = eval ((algebraMap R R') x) (U R' n)

@[simp]

theorem Polynomial.Chebyshev.algebraMap_eval_C {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [Algebra R R'] (x : R) (n : ℤ) : (algebraMap R R') (eval x (C R n)) = eval ((algebraMap R R') x) (C R' n)

@[simp]

theorem Polynomial.Chebyshev.algebraMap_eval_S {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [Algebra R R'] (x : R) (n : ℤ) : (algebraMap R R') (eval x (S R n)) = eval ((algebraMap R R') x) (S R' n)

theorem Polynomial.Chebyshev.T_derivative_eq_U {R : Type u_1} [CommRing R] (n : ℤ) : derivative (T R n) = ↑n * 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 - X ^ 2) * derivative (T R (n + 1)) = (↑n + 1) * (T R n - X * T R (n + 1))

theorem Polynomial.Chebyshev.add_one_mul_T_eq_poly_in_U {R : Type u_1} [CommRing R] (n : ℤ) : (↑n + 1) * T R (n + 1) = X * U R n - (1 - X ^ 2) * derivative (U R n)

theorem Polynomial.Chebyshev.T_mul_T (R : Type u_1) [CommRing R] (m k : ℤ) : 2 * T R m * T R k = T R (m + k) + T R (m - k)

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

theorem Polynomial.Chebyshev.C_mul_C (R : Type u_1) [CommRing R] (m k : ℤ) : C R m * C R k = C R (m + k) + C R (m - k)

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

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

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

theorem Polynomial.Chebyshev.C_mul (R : Type u_1) [CommRing R] (m n : ℤ) : C R (m * n) = (C R m).comp (C R n)

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