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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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)

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

theorem Polynomial.Chebyshev.C_eval_neg_two (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.eval (-2) (Polynomial.Chebyshev.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 : ℤ) : Polynomial.Chebyshev.C R n = 2 * (Polynomial.Chebyshev.T R n).comp (Polynomial.C ⅟2 * Polynomial.X)

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

theorem Polynomial.Chebyshev.C_eq_S_sub_X_mul_S (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.C R n = 2 * Polynomial.Chebyshev.S R n - Polynomial.X * Polynomial.Chebyshev.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 : ℤ) : Polynomial.map f (Polynomial.Chebyshev.T R n) = Polynomial.Chebyshev.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 : ℤ) : Polynomial.map f (Polynomial.Chebyshev.U R n) = Polynomial.Chebyshev.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 : ℤ) : Polynomial.map f (Polynomial.Chebyshev.C R n) = Polynomial.Chebyshev.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 : ℤ) : Polynomial.map f (Polynomial.Chebyshev.S R n) = Polynomial.Chebyshev.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 : ℤ) : (Polynomial.aeval x) (Polynomial.Chebyshev.T R n) = Polynomial.eval x (Polynomial.Chebyshev.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 : ℤ) : (Polynomial.aeval x) (Polynomial.Chebyshev.U R n) = Polynomial.eval x (Polynomial.Chebyshev.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 : ℤ) : (Polynomial.aeval x) (Polynomial.Chebyshev.C R n) = Polynomial.eval x (Polynomial.Chebyshev.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 : ℤ) : (Polynomial.aeval x) (Polynomial.Chebyshev.S R n) = Polynomial.eval x (Polynomial.Chebyshev.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') (Polynomial.eval x (Polynomial.Chebyshev.T R n)) = Polynomial.eval ((algebraMap R R') x) (Polynomial.Chebyshev.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') (Polynomial.eval x (Polynomial.Chebyshev.U R n)) = Polynomial.eval ((algebraMap R R') x) (Polynomial.Chebyshev.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') (Polynomial.eval x (Polynomial.Chebyshev.C R n)) = Polynomial.eval ((algebraMap R R') x) (Polynomial.Chebyshev.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') (Polynomial.eval x (Polynomial.Chebyshev.S R n)) = Polynomial.eval ((algebraMap R R') x) (Polynomial.Chebyshev.S R' 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.T_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.

@[deprecated Polynomial.Chebyshev.T_mul_T]

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)

Alias of Polynomial.Chebyshev.T_mul_T.

---

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 : ℤ) : Polynomial.Chebyshev.C R m * Polynomial.Chebyshev.C R k = Polynomial.Chebyshev.C R (m + k) + Polynomial.Chebyshev.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 : ℤ) : 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.

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

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