U_real_cos — Mathlib

English

Let θ be a real number and n an integer. The n-th Chebyshev polynomial of the second kind evaluated at cos θ, when multiplied by sin θ, equals sin((n+1) θ).

Русский

Пусть θ — вещественное число и n — целое число. n-й полином Чебышёва второго рода в точке cos θ, умноженный на sin θ, равен sin((n+1) θ).

LaTeX

$$$$U_n(\\cos \\theta) \\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_real_cos : (U ℝ n).eval (cos θ) * sin θ = sin ((n + 1) * θ) :=
  mod_cast U_complex_cos θ n

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