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.

source
@[simp]
theorem polynomial.chebyshev.aeval_T {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring 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} [comm_ring R] [comm_ring 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.algebra_map_eval_T {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (x : R) (n : ℕ) :
⇑(algebra_map R A) (polynomial.eval x (polynomial.chebyshev.T R n)) = polynomial.eval (⇑(algebra_map R A) x) (polynomial.chebyshev.T A n)
source
@[simp]
theorem polynomial.chebyshev.algebra_map_eval_U {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (x : R) (n : ℕ) :
⇑(algebra_map R A) (polynomial.eval x (polynomial.chebyshev.U R n)) = polynomial.eval (⇑(algebra_map R A) x) (polynomial.chebyshev.U A n)
source
@[simp, norm_cast]
theorem polynomial.chebyshev.complex_of_real_eval_T (x : ℝ) (n : ℕ) :
↑(polynomial.eval x (polynomial.chebyshev.T ℝ n)) = polynomial.eval ↑x (polynomial.chebyshev.T ℂ n)
source
@[simp, norm_cast]
theorem polynomial.chebyshev.complex_of_real_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 θ.

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 θ.