Multiple angle formulas in terms of Chebyshev polynomials

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Complex versions

@[simp]

theorem Polynomial.Chebyshev.T_complex_cos (θ : ℂ) (n : ℤ) : eval (Complex.cos θ) (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 : ℤ) : eval (Complex.cos θ) (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 : ℤ) : eval (2 * Complex.cos θ) (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 : ℤ) : eval (2 * Complex.cos θ) (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 θ.

@[simp]

theorem Polynomial.Chebyshev.T_complex_cosh (θ : ℂ) (n : ℤ) : eval (Complex.cosh θ) (T ℂ n) = Complex.cosh (↑n * θ)

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

@[simp]

theorem Polynomial.Chebyshev.U_complex_cosh (θ : ℂ) (n : ℤ) : eval (Complex.cosh θ) (U ℂ n) * Complex.sinh θ = Complex.sinh ((↑n + 1) * θ)

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

@[simp]

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

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

@[simp]

theorem Polynomial.Chebyshev.S_two_mul_complex_cosh (θ : ℂ) (n : ℤ) : eval (2 * Complex.cosh θ) (S ℂ n) * Complex.sinh θ = Complex.sinh ((↑n + 1) * θ)

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

Real versions

@[simp]

theorem Polynomial.Chebyshev.T_real_cos (θ : ℝ) (n : ℤ) : eval (Real.cos θ) (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 : ℤ) : eval (Real.cos θ) (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 : ℤ) : eval (2 * Real.cos θ) (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 : ℤ) : eval (2 * Real.cos θ) (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 θ.

@[simp]

theorem Polynomial.Chebyshev.T_real_cosh (θ : ℝ) (n : ℤ) : eval (Real.cosh θ) (T ℝ n) = Real.cosh (↑n * θ)

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

@[simp]

theorem Polynomial.Chebyshev.U_real_cosh (θ : ℝ) (n : ℤ) : eval (Real.cosh θ) (U ℝ n) * Real.sinh θ = Real.sinh ((↑n + 1) * θ)

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

@[simp]

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

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

@[simp]

theorem Polynomial.Chebyshev.S_two_mul_real_cosh (θ : ℝ) (n : ℤ) : eval (2 * Real.cosh θ) (S ℝ n) * Real.sinh θ = Real.sinh ((↑n + 1) * θ)

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