U_sub_two — Mathlib

English

For every integer n, the backward recurrence U_{n-2} = 2X U_{n-1} − U_n holds for Chebyshev polynomials of the second kind.

Русский

Для каждого целого n выполняется обратная рекуррентная формула U_{n-2} = 2X U_{n-1} − U_n для полиномов Чебышёва второго рода.

LaTeX

$$$ U(n-2) = 2X\,U(n-1) - U(n) $$$

Lean4

theorem U_sub_two (n : ℤ) : U R (n - 2) = 2 * X * U R (n - 1) - U R n := by
  linear_combination (norm := ring_nf) U_add_two R (n - 2)

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