mathlib3 documentation

analysis.special_functions.trigonometric.chebyshev

Multiple angle formulas in terms of Chebyshev polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file gives the trigonometric characterizations of Chebyshev polynomials, for both the real (real.cos) and complex (complex.cos) cosine.

Complex versions #

@[simp]

The n-th Chebyshev polynomial of the first kind evaluates on cos θ to the value cos (n * θ).

@[simp]

The n-th Chebyshev polynomial of the second kind evaluates on cos θ to the value sin ((n + 1) * θ) / sin θ.

@[simp]

The n-th Chebyshev polynomial of the first kind evaluates on cos θ to the value cos (n * θ).

@[simp]

The n-th Chebyshev polynomial of the second kind evaluates on cos θ to the value sin ((n + 1) * θ) / sin θ.