The Chebyshev polynomials as a basis

This file packages the Chebyshev polynomials of the first kind as a basis of R[X] when R is an integral domain in which 2 is invertible. Mathlib already proves that T R n has degree n, records its leading coefficient, and bundles the family as Polynomial.Chebyshev.chebyshevTsequence. Its generic polynomial-sequence API then gives a basis whenever all leading coefficients are units.

The resulting basis is an algebraic prerequisite for Part C of the OrthogonalL2Bases roadmap.

Main declarations

• Polynomial.Chebyshev.chebyshevTBasis: the basis n ↦ T R n of R[X];

noncomputable def Polynomial.Chebyshev.chebyshevTBasis {R : Type u_1} [CommRing R] [IsDomain R] [Invertible 2] : Module.Basis ℕ R (Polynomial R)

The Chebyshev polynomials of the first kind, indexed by their nonnegative degree, form a basis of R[X].

Equations

• Polynomial.Chebyshev.chebyshevTBasis = (Polynomial.Chebyshev.chebyshevTsequence R).basis ⋯

@[simp]

theorem Polynomial.Chebyshev.chebyshevTBasis_apply {R : Type u_1} [CommRing R] [IsDomain R] [Invertible 2] (n : ℕ) : chebyshevTBasis n = T R ↑n

The nth vector of the Chebyshev basis is T R n.