# mathlib3documentation

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.

@[simp]
theorem polynomial.chebyshev.aeval_T {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (x : A) (n : ) :
=
@[simp]
theorem polynomial.chebyshev.aeval_U {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (x : A) (n : ) :
=
@[simp]
theorem polynomial.chebyshev.algebra_map_eval_T {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (x : R) (n : ) :
A) n)) = polynomial.eval ( A) x)
@[simp]
theorem polynomial.chebyshev.algebra_map_eval_U {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (x : R) (n : ) :
A) n)) = polynomial.eval ( A) x)
@[simp, norm_cast]
@[simp, norm_cast]

### Complex versions #

@[simp]
theorem polynomial.chebyshev.T_complex_cos (θ : ) (n : ) :

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

@[simp]
theorem polynomial.chebyshev.U_complex_cos (θ : ) (n : ) :
= complex.sin ((n + 1) * θ)

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

@[simp]
theorem polynomial.chebyshev.T_real_cos (θ : ) (n : ) :
= real.cos (n * θ)

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

@[simp]
theorem polynomial.chebyshev.U_real_cos (θ : ) (n : ) :
= real.sin ((n + 1) * θ)

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