### Abstract

The multiple-angle formulas for $\cos$ and $\sin$ state that for any natural number $n$, the values of $\cos nx$ and $\sin nx$ can be expressed in terms of $\cos x$ 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 for any monic polynomial $p$ of degree $n > 0$, it holds that $\sup_{x\in[-1,1]} |p(x)| \geq 2^{n-1}$, 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.

### License

BSD License

### Topics

- Mathematics/Algebra

### Session Chebyshev_Polynomials

- Polynomial_Transfer
- Chebyshev_Polynomials_Library
- Chebyshev_Polynomials

### Depends on

- Descartes' Rule of Signs
- Polynomial Interpolation

## Cite

×

Chebyshev_Polynomials-AFP

    @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},
    }

Download

## Download

× Download latest