English
The S-polynomials are the second-kind Chebyshev polynomials, defined on the integers by S(0)=1, S(1)=X, and the recurrences S(n+2)=X S(n+1)−S(n) and S(−(n+1))=X S(−n)−S(−n+1).
Русский
Полиномы S — это вторые полиномы Чебышёва, определённые на множесте целых чисел: S(0)=1, S(1)=X, а затем S(n+2)=X S(n+1)−S(n) и S(−(n+1))=X S(−n)−S(−n+1).
LaTeX
$$$ S: \mathbb{Z} \to R[X] \quad\text{с заданием } S(0)=1,\ S(1)=X,\ S(n+2)=X\,S(n+1)-S(n),\ S(-\,(n+1))=X\,S(-n)-S(-n+1). $$$$
Lean4
/-- `S n` is the `n`th rescaled Chebyshev polynomial of the second kind (also known as a
Vieta–Fibonacci polynomial), given by $S_n(2x) = U_n(x)$. See
`Polynomial.Chebyshev.S_comp_two_mul_X`. -/
noncomputable def S : ℤ → R[X]
| 0 => 1
| 1 => X
| (n : ℕ) + 2 => X * S (n + 1) - S n
| -((n : ℕ) + 1) => X * S (-n) - S (-n + 1)
termination_by n => Int.natAbs n + Int.natAbs (n - 1)
