Addition and divisibility for the rescaled Chebyshev polynomials of the second kind

Mathlib's rescaled Chebyshev polynomial of the second kind Polynomial.Chebyshev.S R n satisfies (u - u⁻¹) Sₙ(u + u⁻¹) = uⁿ⁺¹ - u⁻ⁿ⁻¹, so Sₙ₋₁ is the symmetric quantum integer [n] as a polynomial in u + u⁻¹. This file proves, over an arbitrary commutative ring and for all integer indices, the polynomial identities behind the arithmetic of quantum integers:

• the addition formula S_{m+n} = Sₘ Sₙ - S_{m-1} S_{n-1}, which is [m + n + 1] = [m + 1] [n + 1] - [m] [n];
• the product with the rescaled Chebyshev polynomial of the first kind, Cₘ Sₙ = S_{n+m} + S_{n-m}, the analogue of Mathlib's Polynomial.Chebyshev.C_mul_C;
• the multiplication formula S_{mn-1} = S_{m-1} · (S_{n-1} ∘ Cₘ), which is [mn]_u = [m]_u [n]_{uᵐ}, since Cₘ(u + u⁻¹) = uᵐ + u⁻ᵐ;
• hence the divisibility S_{m-1} ∣ S_{n-1} whenever m ∣ n, that is [m] ∣ [n].

Being identities of polynomials, they specialize to every evaluation, in particular to quantum integers at an arbitrary loop parameter δ = u + u⁻¹.

Main results

• Polynomial.Chebyshev.S_add: S_{m+n} = Sₘ Sₙ - S_{m-1} S_{n-1}.
• Polynomial.Chebyshev.C_mul_S: Cₘ Sₙ = S_{n+m} + S_{n-m}.
• Polynomial.Chebyshev.S_mul_sub_one: S_{mn-1} = S_{m-1} · (S_{n-1} ∘ Cₘ).
• Polynomial.Chebyshev.S_sub_one_dvd_S_sub_one: m ∣ n → S_{m-1} ∣ S_{n-1}.

References

• J. C. Mason and D. C. Handscomb, Chebyshev Polynomials, Chapman & Hall/CRC, 2003, for the product and composition identities of the Chebyshev polynomials.

theorem Polynomial.Chebyshev.S_add (R : Type u_1) [CommRing R] (m n : ℤ) : S R (m + n) = S R m * S R n - S R (m - 1) * S R (n - 1)

Addition formula for the rescaled Chebyshev polynomials of the second kind: S_{m+n} = Sₘ Sₙ - S_{m-1} S_{n-1}. In quantum-integer form this is [m + n + 1] = [m + 1] [n + 1] - [m] [n].

theorem Polynomial.Chebyshev.C_mul_S (R : Type u_1) [CommRing R] (m n : ℤ) : C R m * S R n = S R (n + m) + S R (n - m)

The product of a rescaled Chebyshev polynomial of the first kind with one of the second kind: Cₘ Sₙ = S_{n+m} + S_{n-m}.

theorem Polynomial.Chebyshev.S_mul_sub_one (R : Type u_1) [CommRing R] (m n : ℤ) : S R (m * n - 1) = S R (m - 1) * (S R (n - 1)).comp (C R m)

Multiplication formula for the rescaled Chebyshev polynomials of the second kind: S_{mn-1} = S_{m-1} · (S_{n-1} ∘ Cₘ). In quantum-integer form, since Cₘ(u + u⁻¹) = uᵐ + u⁻ᵐ, this is [mn]_u = [m]_u [n]_{uᵐ}.

theorem Polynomial.Chebyshev.S_sub_one_dvd_S_sub_one (R : Type u_1) [CommRing R] {m n : ℤ} (h : m ∣ n) : S R (m - 1) ∣ S R (n - 1)

Divisibility of the rescaled Chebyshev polynomials of the second kind: if m ∣ n then S_{m-1} ∣ S_{n-1}. In quantum-integer form, [m] ∣ [n] whenever m ∣ n.