S_two_mul_real_cosh — Mathlib

English

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

Русский

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

LaTeX

$$$$S_n(2 \\cosh \\theta) \\sinh \\theta = \\sinh((n+1) \\theta)$$$$

Lean4

/-- The `n`-th rescaled Chebyshev polynomial of the second kind (Vieta–Fibonacci polynomial)
evaluates on `2 * cosh θ` to the value `sinh ((n + 1) * θ) / sinh θ`. -/
@[simp]
theorem S_two_mul_real_cosh (n : ℤ) : (S ℝ n).eval (2 * cosh θ) * sinh θ = sinh ((n + 1) * θ) :=
  mod_cast S_two_mul_complex_cosh θ n

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