T_add_two — Mathlib

English

Recurrence for T with +2 step, mirroring T_add_two for integers as in previous item.

Русский

Рекуррентное соотношение для T при добавлении 2; аналогично предыдущему пункту.

LaTeX

$$$T_R(n+2) = 2 \\cdot X \\cdot T_R(n+1) - T_R(n)$$$

Lean4

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

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