U_real_cosh — Mathlib

English

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

Русский

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

LaTeX

$$$$U_n(\\cosh \\theta) \\sinh \\theta = \\sinh((n+1) \\theta)$$$$

Lean4

/-- The `n`-th Chebyshev polynomial of the second kind evaluates on `cosh θ` to the
value `sinh ((n + 1) * θ) / sinh θ`. -/
@[simp]
theorem U_real_cosh (n : ℤ) : (U ℝ n).eval (cosh θ) * sinh θ = sinh ((n + 1) * θ) :=
  mod_cast U_complex_cosh θ n

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