Abstract

The multiple-angle formulas for the sine and cosine functions state that for any natural number n, the values of cos(nx) and sin(nx) and can be expressed in terms cos(x) of and sin(x). To be more precise, there are polynomials T(n) and U(n) such that cos(nx) = T(n, cos(x)) and sin(nx) = U(n, cos(x)) sin(x). These are called the Chebyshev polynomials of the first and second kind, respectively.

This entry contains a definition of these two familes of polynomials in Isabelle/HOL along with some of their most important properties. In particular, it is shown that T(n) and U(n) are orthogonal families of polynomials.

Moreover, we show the well-known result that monic polynomial of degree has a supremum norm of at least 2^(n-1) on the unit interval , and that this inequality is sharp since equality holds with p = 2^(1-n) T(n). This has important consequences in the theory of function interpolation, since it implies that the roots of T(n) (also colled the Chebyshev nodes) are exceptionally well-suited as interpolation nodes.

BibTeX

@article{Chebyshev_Polynomials-AFP,
  author  = {Manuel Eberl},
  title   = {Chebyshev Polynomials},
  journal = {Archive of Formal Proofs},
  month   = {November},
  year    = {2023},
  note    = {\url{https://isa-afp.org/entries/Chebyshev_Polynomials.html},
             Formal proof development},
  ISSN    = {2150-914x},
}