Evaluating the Dickson polynomials of the second kind

The Eichler–Selberg weights P_k(t, a), defined by ∑_{k ≥ 2} P_k(t, a) x ^ (k - 2) = (1 - t x + a x²)⁻¹, are the Dickson values (dickson 2 a (k - 2)).eval t, so no new polynomial family is introduced for them. This file proves the generating function and the closed forms the trace formula consumes. The central one is the evaluation at a sum x + y with x * y = a: when t and a are the trace and determinant of a 2 × 2 matrix with eigenvalues x and y, the weight P_{n+2}(t, a) is the trace of the matrix on homogeneous polynomials of degree n.

Main results

• Polynomial.dickson_two_eval_add: if x * y = a, then (dickson 2 a n).eval (x + y) = ∑ i ∈ range (n + 1), x ^ i * y ^ (n - i).
• Polynomial.dickson_two_eval_add_mul_sub: if x * y = a, then (dickson 2 a n).eval (x + y) * (x - y) = x ^ (n + 1) - y ^ (n + 1), the quotient formula with the division cleared.
• Polynomial.dickson_two_sq_eval_two_mul: (dickson 2 (x ^ 2) n).eval (2 * x) = (n + 1) * x ^ n, the repeated-root case t² = 4 a, where the quotient formula says nothing.
• Polynomial.dickson_sq_mul_eval_mul: for every kind k, (dickson k (s ^ 2 * a) n).eval (s * t) = s ^ n * (dickson k a n).eval t.
• Polynomial.dickson_two_sq_eval_mul: (dickson 2 (s ^ 2) n).eval (s * t) = s ^ n * (Chebyshev.S R n).eval t, the division-free form of P_k(t, s²) = s ^ (k - 2) * U_{k-2}(t / (2 s)).
• Polynomial.mk_dickson_two_eval_mul_one_sub_add_eq_one: the generating function (∑ₙ (dickson 2 a n).eval t * Xⁿ) * (1 - t X + a X²) = 1.
• Polynomial.dickson_two_one_eval_zero_two_mul, Polynomial.dickson_two_one_eval_one_add_three, Polynomial.dickson_two_one_eval_neg_one_add_three: the weights P_{n+2}(t, 1) at the traces t = 0, 1, -1 of the elliptic elements of SL(2, ℤ), which have periods 4, 6 and 3 in n (Polynomial.dickson_two_one_eval_one_six_mul_add, Polynomial.dickson_two_one_eval_neg_one_three_mul_add).

References

• D. Zagier, The Eichler–Selberg trace formula on SL₂(ℤ), appendix to S. Lang, Introduction to Modular Forms, Springer, 1976.
• A. Popa and D. Zagier, An elementary proof of the Eichler–Selberg trace formula, J. Reine Angew. Math. 762 (2020), 105–122, arXiv:1711.00327.

theorem Polynomial.dickson_two_eval_add {R : Type u_1} [CommRing R] {x y a : R} (h : x * y = a) (n : ℕ) : eval (x + y) (dickson 2 a n) = ∑ i ∈ Finset.range (n + 1), x ^ i * y ^ (n - i)

The Dickson polynomial of the second kind at x + y is the complete homogeneous symmetric polynomial in x and y, when its parameter is x * y.

When x and y are the eigenvalues of a 2 × 2 matrix, x + y and x * y are its trace and determinant, and the right side is the trace of the matrix on homogeneous polynomials of degree n; this is how the Eichler–Selberg weights enter as traces. The right side is the value of the complete homogeneous symmetric polynomial MvPolynomial.hsymm at ![x, y], as computed by TauCeti.eval_hsymm_fin_two. Compare Mathlib's dickson_one_one_eval_add_inv, the first-kind analogue for x * y = 1, where the value is the power sum x ^ n + y ^ n.

theorem Polynomial.dickson_two_eval_add_mul_sub {R : Type u_1} [CommRing R] {x y a : R} (h : x * y = a) (n : ℕ) : eval (x + y) (dickson 2 a n) * (x - y) = x ^ (n + 1) - y ^ (n + 1)

The Dickson value times x - y is x ^ (n + 1) - y ^ (n + 1), when x * y = a.

This is the quotient formula P_k(t, a) = (x ^ (k - 1) - y ^ (k - 1)) / (x - y) for the roots x, y of X² - t X + a, stated multiplied out so that it holds in any commutative ring and at a repeated root; for the value at a repeated root itself use dickson_two_sq_eval_two_mul, and for the quotient itself, over a field at distinct roots, dickson_two_eval_add_eq_div.

theorem Polynomial.dickson_two_eval_add_eq_div {K : Type u_2} [Field K] {x y a : K} (h : x * y = a) (hxy : x ≠ y) (n : ℕ) : eval (x + y) (dickson 2 a n) = (x ^ (n + 1) - y ^ (n + 1)) / (x - y)

The quotient formula at distinct roots: over a field, if x * y = a and x ≠ y, then (dickson 2 a n).eval (x + y) = (x ^ (n + 1) - y ^ (n + 1)) / (x - y).

@[simp]

theorem Polynomial.dickson_two_sq_eval_two_mul {R : Type u_1} [CommRing R] (x : R) (n : ℕ) : eval (2 * x) (dickson 2 (x ^ 2) n) = (↑n + 1) * x ^ n

At a repeated root the Dickson value is (n + 1) * x ^ n: this is the value at t = 2 * x with parameter a = x ^ 2, where X² - t X + a = (X - x)² has the repeated root x.

These are the t² = 4 a terms P_k(2 x, x²) = (k - 1) * x ^ (k - 2) of the Eichler–Selberg trace formula, where dickson_two_eval_add_mul_sub degenerates to 0 = 0. The other sign, t = -2 * x, is the case -x, since (-x) ^ 2 = x ^ 2.

@[simp]

theorem Polynomial.dickson_sq_mul_eval_mul {R : Type u_1} [CommRing R] (k : ℕ) (s t a : R) (n : ℕ) : eval (s * t) (dickson k (s ^ 2 * a) n) = s ^ n * eval t (dickson k a n)

The Dickson polynomials are homogeneous of degree n when the parameter is given weight two: for every kind k, scaling the argument by s and the parameter by s ^ 2 scales the value by s ^ n.

@[simp]

theorem Polynomial.dickson_two_sq_eval_mul {R : Type u_1} [CommRing R] (s t : R) (n : ℕ) : eval (s * t) (dickson 2 (s ^ 2) n) = s ^ n * eval t (Chebyshev.S R ↑n)

The Dickson polynomial of the second kind with square parameter is a rescaled Chebyshev polynomial.

Since Chebyshev.S R n is U_n(X / 2), this is the division-free form of the identity P_k(t, s²) = s ^ (k - 2) * U_{k-2}(t / (2 s)) relating the Eichler–Selberg weights to the Chebyshev polynomials of the second kind; at s = 1 it is Mathlib's dickson_two_one_eq_chebyshev_S evaluated at t. For Chebyshev.U itself take 2 * t for t: Chebyshev.S_comp_two_mul_X and eval_comp turn (Chebyshev.S R n).eval (2 * t) into (Chebyshev.U R n).eval t without inverting 2.

theorem Polynomial.mk_dickson_two_eval_mul_one_sub_add_eq_one {R : Type u_1} [CommRing R] (t a : R) : (PowerSeries.mk fun (n : ℕ) => eval t (dickson 2 a n)) * (1 - PowerSeries.C t * PowerSeries.X + PowerSeries.C a * PowerSeries.X ^ 2) = 1

The generating function of the Dickson values: (∑ₙ (dickson 2 a n).eval t * Xⁿ) * (1 - t X + a X²) = 1 in R⟦X⟧.

This identifies the Eichler–Selberg weights with the Dickson values in any commutative ring, with no inverse taken. Over a field, PowerSeries.eq_inv_iff_mul_eq_one turns it into PowerSeries.mk (fun n ↦ (dickson 2 a n).eval t) = (1 - C t * X + C a * X ^ 2)⁻¹.

The weights at the traces 0 and ±1

The elliptic elements S = !![0, -1; 1, 0], U = !![1, -1; 1, 0] and U² = !![0, -1; 1, -1] of SL(2, ℤ) have traces 0, 1 and -1, so their traces on binary forms of degree n are the weights P_{n+2}(0, 1), P_{n+2}(1, 1) and P_{n+2}(-1, 1). With parameter 1 the recurrence makes these periodic in n.

@[simp]

theorem Polynomial.dickson_two_one_eval_zero_two_mul {R : Type u_1} [CommRing R] (m : ℕ) : eval 0 (dickson 2 1 (2 * m)) = (-1) ^ m

P_{2m+2}(0, 1) = (-1) ^ m.

theorem Polynomial.dickson_two_one_eval_one_add_three {R : Type u_1} [CommRing R] (n : ℕ) : eval 1 (dickson 2 1 (n + 3)) = -eval 1 (dickson 2 1 n)

P_{n+5}(1, 1) = -P_{n+2}(1, 1), so n ↦ P_{n+2}(1, 1) has period 6.

theorem Polynomial.dickson_two_one_eval_neg_one_add_three {R : Type u_1} [CommRing R] (n : ℕ) : eval (-1) (dickson 2 1 (n + 3)) = eval (-1) (dickson 2 1 n)

P_{n+5}(-1, 1) = P_{n+2}(-1, 1): n ↦ P_{n+2}(-1, 1) has period 3.

@[simp]

theorem Polynomial.dickson_two_one_eval_one_six_mul_add {R : Type u_1} [CommRing R] (j r : ℕ) : eval 1 (dickson 2 1 (6 * j + r)) = eval 1 (dickson 2 1 r)

P_{n+2}(1, 1) has period 6 in n.

@[simp]

theorem Polynomial.dickson_two_one_eval_neg_one_three_mul_add {R : Type u_1} [CommRing R] (j r : ℕ) : eval (-1) (dickson 2 1 (3 * j + r)) = eval (-1) (dickson 2 1 r)

P_{n+2}(-1, 1) has period 3 in n.