Chebyshev polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The Chebyshev polynomials are two 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, the product of them-th and(m + k)-th Chebyshev polynomials of the first kind is the sum of the(2 * m + k)-th andk-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 them-th andn-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.cast_ring_hom R) interfering all the time.
References #
Lionel Ponton, Roots of the Chebyshev polynomials: A purely algebraic approach
TODO #
- Redefine and/or relate the definition of Chebyshev polynomials to
linear_recurrence. - 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.
T n is the n-th Chebyshev polynomial of the first kind
Equations
- polynomial.chebyshev.T R (n + 2) = 2 * polynomial.X * polynomial.chebyshev.T R n.succ - polynomial.chebyshev.T R n
- polynomial.chebyshev.T R 1 = polynomial.X
- polynomial.chebyshev.T R 0 = 1
@[simp]
@[simp]
@[simp]
theorem
polynomial.chebyshev.T_add_two
(R : Type u_1)
[comm_ring 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_two
(R : Type u_1)
[comm_ring R] :
polynomial.chebyshev.T R 2 = 2 * polynomial.X ^ 2 - 1
theorem
polynomial.chebyshev.T_of_two_le
(R : Type u_1)
[comm_ring R]
(n : ℕ)
(h : 2 ≤ n) :
polynomial.chebyshev.T R n = 2 * polynomial.X * polynomial.chebyshev.T R (n - 1) - polynomial.chebyshev.T R (n - 2)
U n is the n-th Chebyshev polynomial of the second kind
Equations
- polynomial.chebyshev.U R (n + 2) = 2 * polynomial.X * polynomial.chebyshev.U R n.succ - polynomial.chebyshev.U R n
- polynomial.chebyshev.U R 1 = 2 * polynomial.X
- polynomial.chebyshev.U R 0 = 1
@[simp]
@[simp]
theorem
polynomial.chebyshev.U_one
(R : Type u_1)
[comm_ring R] :
polynomial.chebyshev.U R 1 = 2 * polynomial.X
@[simp]
theorem
polynomial.chebyshev.U_add_two
(R : Type u_1)
[comm_ring 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_two
(R : Type u_1)
[comm_ring R] :
polynomial.chebyshev.U R 2 = 4 * polynomial.X ^ 2 - 1
theorem
polynomial.chebyshev.U_of_two_le
(R : Type u_1)
[comm_ring R]
(n : ℕ)
(h : 2 ≤ n) :
polynomial.chebyshev.U R n = 2 * polynomial.X * polynomial.chebyshev.U R (n - 1) - polynomial.chebyshev.U R (n - 2)
theorem
polynomial.chebyshev.U_eq_X_mul_U_add_T
(R : Type u_1)
[comm_ring 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)
[comm_ring R]
(n : ℕ) :
polynomial.chebyshev.T R (n + 1) = polynomial.chebyshev.U R (n + 1) - polynomial.X * polynomial.chebyshev.U R n
theorem
polynomial.chebyshev.T_eq_X_mul_T_sub_pol_U
(R : Type u_1)
[comm_ring 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)
[comm_ring 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}
[comm_ring R]
[comm_ring 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}
[comm_ring R]
[comm_ring 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}
[comm_ring R]
(n : ℕ) :
⇑polynomial.derivative (polynomial.chebyshev.T R (n + 1)) = (↑n + 1) * polynomial.chebyshev.U R n
theorem
polynomial.chebyshev.one_sub_X_sq_mul_derivative_T_eq_poly_in_T
{R : Type u_1}
[comm_ring 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}
[comm_ring 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)
[comm_ring R]
(m k : ℕ) :
2 * polynomial.chebyshev.T R m * polynomial.chebyshev.T R (m + k) = polynomial.chebyshev.T R (2 * m + k) + polynomial.chebyshev.T R k
The product of two Chebyshev polynomials is the sum of two other Chebyshev polynomials.
theorem
polynomial.chebyshev.T_mul
(R : Type u_1)
[comm_ring 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 polynomial is the composition of the m-th and n-th