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

@[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.

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.

theorem Polynomial.Chebyshev.induct' (motive : ℤ → Prop) (zero : motive 0) (one : motive 1) (add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)) (neg : ∀ (n : ℤ), motive n → motive (-n)) (a : ℤ) : motive a

Another induction principle used for proving facts about Chebyshev polynomials, which is sometimes easier to use

@[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

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

theorem Polynomial.Chebyshev.T_eval_zero (R : Type u_1) [CommRing R] (n : ℤ) : eval 0 (T R n) = ↑(if Even n then ↑(n / 2).negOnePow else 0)

@[simp]

theorem Polynomial.Chebyshev.T_eval_zero_of_even (R : Type u_1) [CommRing R] {n : ℤ} (hn : Even n) : eval 0 (T R n) = ↑↑(n / 2).negOnePow

theorem Polynomial.Chebyshev.T_eval_two_mul_zero (R : Type u_1) [CommRing R] (n : ℤ) : eval 0 (T R (2 * n)) = ↑↑n.negOnePow

@[simp]

theorem Polynomial.Chebyshev.T_eval_zero_of_odd (R : Type u_1) [CommRing R] {n : ℤ} (hn : Odd n) : eval 0 (T R n) = 0

@[simp]

theorem Polynomial.Chebyshev.degree_T (R : Type u_1) [CommRing R] [IsDomain R] [NeZero 2] (n : ℤ) : (T R n).degree = ↑n.natAbs

@[simp]

theorem Polynomial.Chebyshev.natDegree_T (R : Type u_1) [CommRing R] [IsDomain R] [NeZero 2] (n : ℤ) : (T R n).natDegree = n.natAbs

@[simp]

theorem Polynomial.Chebyshev.leadingCoeff_T (R : Type u_1) [CommRing R] [IsDomain R] [NeZero 2] (n : ℤ) : (T R n).leadingCoeff = 2 ^ (n.natAbs - 1)

@[simp]

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

theorem Polynomial.Chebyshev.T_ne_zero (R : Type u_1) [CommRing R] (n : ℤ) [IsDomain R] [NeZero 2] : T R n ≠ 0

noncomputable def Polynomial.Chebyshev.chebyshevTsequence (R : Type u_1) [CommRing R] [IsDomain R] [NeZero 2] : Sequence R

ChebyshevT as a polynomial sequence.

@[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.

@[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

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_eval_zero (R : Type u_1) [CommRing R] (n : ℤ) : eval 0 (U R n) = ↑(if Even n then ↑(n / 2).negOnePow else 0)

@[simp]

theorem Polynomial.Chebyshev.U_eval_zero_of_even (R : Type u_1) [CommRing R] {n : ℤ} (hn : Even n) : eval 0 (U R n) = ↑↑(n / 2).negOnePow

theorem Polynomial.Chebyshev.U_eval_two_mul_zero (R : Type u_1) [CommRing R] (n : ℤ) : eval 0 (U R (2 * n)) = ↑↑n.negOnePow

@[simp]

theorem Polynomial.Chebyshev.U_eval_zero_of_odd (R : Type u_1) [CommRing R] {n : ℤ} (hn : Odd n) : eval 0 (U R n) = 0

@[simp]

theorem Polynomial.Chebyshev.degree_U_natCast (R : Type u_1) [CommRing R] [IsDomain R] [NeZero 2] (n : ℕ) : (U R ↑n).degree = ↑n

@[simp]

theorem Polynomial.Chebyshev.natDegree_U_natCast (R : Type u_1) [CommRing R] [IsDomain R] [NeZero 2] (n : ℕ) : (U R ↑n).natDegree = n

theorem Polynomial.Chebyshev.degree_U_neg_one (R : Type u_1) [CommRing R] : (U R (-1)).degree = ⊥

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

theorem Polynomial.Chebyshev.degree_U_of_ne_neg_one (R : Type u_1) [CommRing R] [IsDomain R] [NeZero 2] (n : ℤ) (hn : n ≠ -1) : (U R n).degree = ↑((n + 1).natAbs - 1)

theorem Polynomial.Chebyshev.natDegree_U (R : Type u_1) [CommRing R] [IsDomain R] [NeZero 2] (n : ℤ) : (U R n).natDegree = (n + 1).natAbs - 1

@[simp]

theorem Polynomial.Chebyshev.leadingCoeff_U_natCast (R : Type u_1) [CommRing R] [IsDomain R] [NeZero 2] (n : ℕ) : (U R ↑n).leadingCoeff = 2 ^ n

@[simp]

theorem Polynomial.Chebyshev.U_eval_neg (R : Type u_1) [CommRing R] (n : ℕ) (x : R) : eval (-x) (U R ↑n) = ↑↑(↑n).negOnePow * eval x (U R ↑n)

theorem Polynomial.Chebyshev.U_ne_zero (R : Type u_1) [CommRing R] (n : ℤ) [IsDomain R] [NeZero 2] (hn : n ≠ -1) : U R n ≠ 0

theorem Polynomial.Chebyshev.U_eq_zero_iff (R : Type u_1) [CommRing R] (n : ℤ) [IsDomain R] [NeZero 2] : U R n = 0 ↔ 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)

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

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

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

theorem Polynomial.Chebyshev.U_mem_span_T (R : Type u_1) [CommRing R] (n : ℕ) : U R ↑n ∈ Submodule.span ℕ ((fun (m : ℕ) => T R ↑m) '' Set.Icc 0 n)

@[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.

@[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.

@[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.T_derivative_mem_span_T {R : Type u_1} [CommRing R] (n : ℕ) : derivative (T R ↑n) ∈ Submodule.span ℕ ((fun (m : ℕ) => T R ↑m) '' Set.Ico 0 n)

theorem Polynomial.Chebyshev.T_iterate_derivative_mem_span_T {R : Type u_1} [CommRing R] (n k : ℕ) : (⇑derivative)^[k] (T R ↑n) ∈ Submodule.span ℕ ((fun (m : ℕ) => T R ↑m) '' Set.Icc 0 (n - k))

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

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

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

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

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

theorem Polynomial.Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eval {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) (x : R) : (1 - x ^ 2) * eval x ((⇑derivative)^[k + 2] (T R n)) = (2 * ↑k + 1) * x * eval x ((⇑derivative)^[k + 1] (T R n)) - (↑n ^ 2 - ↑k ^ 2) * eval x ((⇑derivative)^[k] (T R n))

theorem Polynomial.Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eval {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) (x : R) : (1 - x ^ 2) * eval x ((⇑derivative)^[k + 2] (U R n)) = (2 * ↑k + 3) * x * eval x ((⇑derivative)^[k + 1] (U R n)) - ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval x ((⇑derivative)^[k] (U R n))

theorem Polynomial.Chebyshev.iterate_derivative_T_eval_one_recurrence {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) : (2 * ↑k + 1) * eval 1 ((⇑derivative)^[k + 1] (T R n)) = (↑n ^ 2 - ↑k ^ 2) * eval 1 ((⇑derivative)^[k] (T R n))

theorem Polynomial.Chebyshev.iterate_derivative_U_eval_one_recurrence {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) : (2 * ↑k + 3) * eval 1 ((⇑derivative)^[k + 1] (U R n)) = ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 1 ((⇑derivative)^[k] (U R n))

theorem Polynomial.Chebyshev.iterate_derivative_T_eval_zero_recurrence {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) : eval 0 ((⇑derivative)^[k + 2] (T R n)) = -(↑n ^ 2 - ↑k ^ 2) * eval 0 ((⇑derivative)^[k] (T R n))

theorem Polynomial.Chebyshev.iterate_derivative_U_eval_zero_recurrence {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) : eval 0 ((⇑derivative)^[k + 2] (U R n)) = -((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 0 ((⇑derivative)^[k] (U R n))

theorem Polynomial.Chebyshev.iterate_derivative_T_eval_one {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) : ↑(∏ l ∈ Finset.range k, (2 * l + 1)) * eval 1 ((⇑derivative)^[k] (T R n)) = ↑(∏ l ∈ Finset.range k, (n ^ 2 - ↑l ^ 2))

theorem Polynomial.Chebyshev.iterate_derivative_U_eval_one {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) : ↑(∏ l ∈ Finset.range k, (2 * l + 3)) * eval 1 ((⇑derivative)^[k] (U R n)) = ↑(∏ l ∈ Finset.range k, ((n + 1) ^ 2 - (↑l + 1) ^ 2)) * (↑n + 1)

theorem Polynomial.Chebyshev.derivative_T_eval_one {R : Type u_1} [CommRing R] (n : ℤ) : eval 1 (derivative (T R n)) = ↑n ^ 2

theorem Polynomial.Chebyshev.derivative_U_eval_one {R : Type u_1} [CommRing R] (n : ℤ) : 3 * eval 1 (derivative (U R n)) = (↑n + 2) * (↑n + 1) * ↑n

theorem Polynomial.Chebyshev.iterate_derivative_T_eval_one_eq_div {𝔽 : Type u_3} [Field 𝔽] [CharZero 𝔽] (n : ℤ) (k : ℕ) : eval 1 ((⇑derivative)^[k] (T 𝔽 n)) = ↑(∏ l ∈ Finset.range k, (n ^ 2 - ↑l ^ 2)) / ↑(∏ l ∈ Finset.range k, (2 * l + 1))

theorem Polynomial.Chebyshev.iterate_derivative_U_eval_one_eq_div {𝔽 : Type u_3} [Field 𝔽] [CharZero 𝔽] (n : ℤ) (k : ℕ) : eval 1 ((⇑derivative)^[k] (U 𝔽 n)) = ↑(∏ l ∈ Finset.range k, ((n + 1) ^ 2 - (↑l + 1) ^ 2)) * (↑n + 1) / ↑(∏ l ∈ Finset.range k, (2 * l + 3))

theorem Polynomial.Chebyshev.iterate_derivative_T_eval_one_dvd {𝔽 : Type u_3} [Field 𝔽] (n : ℤ) (k : ℕ) : ↑(∏ l ∈ Finset.range k, (2 * l + 1)) ∣ ↑(∏ l ∈ Finset.range k, (n ^ 2 - ↑l ^ 2))

theorem Polynomial.Chebyshev.iterate_derivative_U_eval_one_dvd {𝔽 : Type u_3} [Field 𝔽] (n : ℤ) (k : ℕ) : ↑(∏ l ∈ Finset.range k, (2 * l + 3)) ∣ ↑(∏ l ∈ Finset.range k, ((n + 1) ^ 2 - (↑l + 1) ^ 2)) * (↑n + 1)

theorem Polynomial.Chebyshev.derivative_U_eval_one_eq_div {𝔽 : Type u_3} [Field 𝔽] [neZero3 : NeZero 3] (n : ℤ) : eval 1 (derivative (U 𝔽 n)) = (↑n + 2) * (↑n + 1) * ↑n / 3

theorem Polynomial.Chebyshev.derivative_U_eval_one_dvd {𝔽 : Type u_3} [Field 𝔽] (n : ℤ) : 3 ∣ (↑n + 2) * (↑n + 1) * ↑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.