Documentation

Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev

Multiple angle formulas in terms of Chebyshev polynomials #

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

source
@[simp]
theorem Polynomial.Chebyshev.aeval_T {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (x : A) (n : ℤ) :
(Polynomial.aeval x) (Polynomial.Chebyshev.T R n) = Polynomial.eval x (Polynomial.Chebyshev.T A n)
source
@[simp]
theorem Polynomial.Chebyshev.aeval_U {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (x : A) (n : ℤ) :
(Polynomial.aeval x) (Polynomial.Chebyshev.U R n) = Polynomial.eval x (Polynomial.Chebyshev.U A n)
source
@[simp]
theorem Polynomial.Chebyshev.algebraMap_eval_T {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (x : R) (n : ℤ) :
(algebraMap R A) (Polynomial.eval x (Polynomial.Chebyshev.T R n)) = Polynomial.eval ((algebraMap R A) x) (Polynomial.Chebyshev.T A n)
source
@[simp]
theorem Polynomial.Chebyshev.algebraMap_eval_U {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (x : R) (n : ℤ) :
(algebraMap R A) (Polynomial.eval x (Polynomial.Chebyshev.U R n)) = Polynomial.eval ((algebraMap R A) x) (Polynomial.Chebyshev.U A n)
source
@[simp]
theorem Polynomial.Chebyshev.complex_ofReal_eval_T (x : ℝ) (n : ℤ) :
↑(Polynomial.eval x (Polynomial.Chebyshev.T ℝ n)) = Polynomial.eval (↑x) (Polynomial.Chebyshev.T ℂ n)
source
@[simp]
theorem Polynomial.Chebyshev.complex_ofReal_eval_U (x : ℝ) (n : ℤ) :
↑(Polynomial.eval x (Polynomial.Chebyshev.U ℝ n)) = Polynomial.eval (↑x) (Polynomial.Chebyshev.U ℂ n)

Complex versions #

source
@[simp]
theorem Polynomial.Chebyshev.T_complex_cos (θ : ℂ) (n : ℤ) :
Polynomial.eval (Complex.cos θ) (Polynomial.Chebyshev.T ℂ n) = Complex.cos (↑n * θ)

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

source
@[simp]
theorem Polynomial.Chebyshev.U_complex_cos (θ : ℂ) (n : ℤ) :
Polynomial.eval (Complex.cos θ) (Polynomial.Chebyshev.U ℂ n) * Complex.sin θ = Complex.sin ((↑n + 1) * θ)

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

Real versions #

source
@[simp]
theorem Polynomial.Chebyshev.T_real_cos (θ : ℝ) (n : ℤ) :
Polynomial.eval (Real.cos θ) (Polynomial.Chebyshev.T ℝ n) = Real.cos (↑n * θ)

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

source
@[simp]
theorem Polynomial.Chebyshev.U_real_cos (θ : ℝ) (n : ℤ) :
Polynomial.eval (Real.cos θ) (Polynomial.Chebyshev.U ℝ n) * Real.sin θ = Real.sin ((↑n + 1) * θ)

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