English
For every commutative ring R there is a family of polynomials U_n ∈ R[X] (n ∈ ℤ) called Chebyshev polynomials of the second kind, defined by U_0 = 1, U_1 = 2X, U_{n+2} = 2X U_{n+1} − U_n for all integers n, with a corresponding relation for negative indices.
Русский
Для каждого коммутативного кольца R существует семейство полиномов U_n ∈ R[X] (n ∈ ℤ), называемых полиномами Чебышева второго рода, задаваемых уравнениями U_0 = 1, U_1 = 2X, U_{n+2} = 2X U_{n+1} − U_n для всех целых n, а для отрицательных индексов дается соответствующее равенство.
LaTeX
$$$ U: \mathbb{Z} \to R[X],\quad U(0)=1,\ U(1)=2X,\ U(n+2)=2X\,U(n+1)-U(n),\ U(-n-1)=2X\,U(-n)-U(-n+1). $$$
Lean4
/-- `U n` is the `n`-th Chebyshev polynomial of the second kind. -/
noncomputable def U : ℤ → R[X]
| 0 => 1
| 1 => 2 * X
| (n : ℕ) + 2 => 2 * X * U (n + 1) - U n
| -((n : ℕ) + 1) => 2 * X * U (-n) - U (-n + 1)
termination_by n => Int.natAbs n + Int.natAbs (n - 1)
