T_complex_cos — Mathlib

English

The n-th Chebyshev polynomial of the first kind satisfies T_n(cos θ) = cos(n θ).

Русский

Полином Чебышёва первого рода удовлетворяет T_n(cos θ) = cos(n θ).

LaTeX

$$$(T \mathbb{C} n).eval(\cos \theta) = \cos(n \theta)$$$

Lean4

/-- The `n`-th Chebyshev polynomial of the first kind evaluates on `cos θ` to the
value `cos (n * θ)`. -/
@[simp]
theorem T_complex_cos (n : ℤ) : (T ℂ n).eval (cos θ) = cos (n * θ) := by
  induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1
    ih2 =>
    simp only [T_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add, cos_add_cos]
    push_cast
    ring_nf
  | neg_add_one n ih1
    ih2 =>
    simp only [T_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add', cos_add_cos]
    push_cast
    ring_nf

Похожие утверждения