Email Gateway (Nov 21 2023 at 14:38): Email Gateway (Nov 21 2023 at 14:38):From: Lawrence Paulson <lp15@cam.ac.uk>
I am happy to announce a new entry, Chebyshev Polynomials, by Manuel Eberl:
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 ... 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. […]
Now online at https://www.isa-afp.org/entries/Chebyshev_Polynomials.html
Larry Paulson
Last updated: Jan 04 2025 at 20:18 UTC