U_add_two — Mathlib

English

For every integer n and commutative ring R, the Chebyshev polynomials of the second kind satisfy the forward recurrence U_{n+2} = 2X U_{n+1} − U_n.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem U_add_two : ∀ n, U R (n + 2) = 2 * X * U R (n + 1) - U R n
  | (k : ℕ) => U.eq_3 R k
  | -(k + 1 : ℕ) => by linear_combination (norm := (simp [Int.negSucc_eq]; ring_nf)) U.eq_4 R k

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