English
The n-th Chebyshev polynomial of the second kind satisfies U_n(cos θ) sin θ = sin((n+1) θ).
Русский
Полином Чебышева второго рода: U_n(cos θ) sin θ = sin((n+1) θ).
LaTeX
$$$(U \mathbb{C} n).eval(\cos \theta) \cdot \sin \theta = \sin((n+1) \theta)$$$
Lean4
/-- The `n`-th Chebyshev polynomial of the second kind evaluates on `cos θ` to the
value `sin ((n + 1) * θ) / sin θ`. -/
@[simp]
theorem U_complex_cos (n : ℤ) : (U ℂ n).eval (cos θ) * sin θ = sin ((n + 1) * θ) := by
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp [one_add_one_eq_two, sin_two_mul]; ring
| add_two n ih1
ih2 =>
simp only [U_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul, mul_assoc, ih1, ih2, sub_eq_iff_eq_add,
sin_add_sin]
push_cast
ring_nf
| neg_add_one n ih1
ih2 =>
simp only [U_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul, mul_assoc, ih1, ih2, sub_eq_iff_eq_add',
sin_add_sin]
push_cast
ring_nf
