T — Mathlib · SciLib

English

For all rings R, integers n, the Chebyshev polynomials satisfy T(n+2) = 2 X T(n+1) − T(n).

Русский

Для всех колец R выполняется тождество Чебышёва T(n+2) = 2 X T(n+1) − T(n).

LaTeX

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

Lean4

/-- `T n` is the `n`-th Chebyshev polynomial of the first kind. -/
noncomputable def T : ℤ → R[X]
  | 0 => 1
  | 1 => X
  | (n : ℕ) + 2 => 2 * X * T (n + 1) - T n
  | -((n : ℕ) + 1) => 2 * X * T (-n) - T (-n + 1)
termination_by n => Int.natAbs n + Int.natAbs (n - 1)

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