Multiple angle formulas in terms of Chebyshev polynomials #
polynomial.chebyshev.T_complex_cos: then-th Chebyshev polynomial evaluates oncomplex.cos θto the valuecomplex.cos (n * θ).
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 * θ).
theorem
polynomial.chebyshev.cos_nat_mul
(n : ℕ)
(θ : ℂ) :
complex.cos ((↑n) * θ) = polynomial.eval (complex.cos θ) (polynomial.chebyshev.T ℂ n)
cos (n * θ) is equal to the n-th Chebyshev polynomial of the first kind evaluated
on cos θ.
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 θ.
theorem
polynomial.chebyshev.sin_nat_succ_mul
(n : ℕ)
(θ : ℂ) :
complex.sin ((↑n + 1) * θ) = (polynomial.eval (complex.cos θ) (polynomial.chebyshev.U ℂ n)) * complex.sin θ
sin ((n + 1) * θ) is equal to sin θ multiplied with the n-th Chebyshev polynomial of the
second kind evaluated on cos θ.