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.

@[simp]

theorem Polynomial.Chebyshev.complex_ofReal_eval_T (x : ℝ) (n : ℤ) : ↑(Polynomial.eval x (Polynomial.Chebyshev.T ℝ n)) = Polynomial.eval (↑x) (Polynomial.Chebyshev.T ℂ n)

@[simp]

theorem Polynomial.Chebyshev.complex_ofReal_eval_U (x : ℝ) (n : ℤ) : ↑(Polynomial.eval x (Polynomial.Chebyshev.U ℝ n)) = Polynomial.eval (↑x) (Polynomial.Chebyshev.U ℂ n)

@[simp]

theorem Polynomial.Chebyshev.complex_ofReal_eval_C (x : ℝ) (n : ℤ) : ↑(Polynomial.eval x (Polynomial.Chebyshev.C ℝ n)) = Polynomial.eval (↑x) (Polynomial.Chebyshev.C ℂ n)

@[simp]

theorem Polynomial.Chebyshev.complex_ofReal_eval_S (x : ℝ) (n : ℤ) : ↑(Polynomial.eval x (Polynomial.Chebyshev.S ℝ n)) = Polynomial.eval (↑x) (Polynomial.Chebyshev.S ℂ n)

Complex versions

@[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 * θ).

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

@[simp]

theorem Polynomial.Chebyshev.C_two_mul_complex_cos (θ : ℂ) (n : ℤ) : Polynomial.eval (2 * Complex.cos θ) (Polynomial.Chebyshev.C ℂ n) = 2 * Complex.cos (↑n * θ)

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

@[simp]

theorem Polynomial.Chebyshev.S_two_mul_complex_cos (θ : ℂ) (n : ℤ) : Polynomial.eval (2 * Complex.cos θ) (Polynomial.Chebyshev.S ℂ n) * Complex.sin θ = Complex.sin ((↑n + 1) * θ)

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

Real versions

@[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 * θ).

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

@[simp]

theorem Polynomial.Chebyshev.C_two_mul_real_cos (θ : ℝ) (n : ℤ) : Polynomial.eval (2 * Real.cos θ) (Polynomial.Chebyshev.C ℝ n) = 2 * Real.cos (↑n * θ)

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

@[simp]

theorem Polynomial.Chebyshev.S_two_mul_real_cos (θ : ℝ) (n : ℤ) : Polynomial.eval (2 * Real.cos θ) (Polynomial.Chebyshev.S ℝ n) * Real.sin θ = Real.sin ((↑n + 1) * θ)

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