The class-number trace formula on period polynomials

This file assembles the trace of Popa–Zagier's explicit element on the full period-polynomial space W_w. For positive even w and n > 0, it is

σ_{w+1}(n) - ∑_{ad=n} min(a,d)^{w+1} - ∑_{t²≤4n} H(4n-t²) P_{w+2}(t,n).

Here Popa–Zagier's P_{w+2}(t,n) is (dickson 2 n w).eval t, the degree-w second-kind Dickson polynomial evaluated at t. The convention H(0) = -1/12 absorbs the repeated-root contribution. The trace is on W_w, not on cusp forms: the latter requires the Hecke-equivariant Eichler–Shimura comparison and subtraction of the Eisenstein eigenvalue, followed by division by two.

The inputs are the fixed-trace assembly in ExplicitElement.Trace and the elliptic, hyperbolic and repeated-root fibre evaluations. Pairing the fibres of traces t and -t removes the sign asymmetry of the explicit representative. Split hyperbolic traces correspond to unordered positive factorizations n = ad; the Dickson root formula changes their contribution into d^{w+1} - a^{w+1}.

References

• 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, §§2, 4.
• D. Zagier, The Eichler–Selberg trace formula on SL₂(ℤ), appendix to S. Lang, Introduction to Modular Forms, for the convention H(0) = -1/12.

theorem TauCeti.TraceFormulaMatrixModule.trace_periodActionRestrict_popaZagierElement_eq_sigma_sub_min_sub_hurwitzClassNumber {K : Type u_1} [Field K] [CharZero K] (n : ℕ) (hn : 0 < n) (w : ℕ) (hw : Even w) (hw₀ : w ≠ 0) : (LinearMap.trace K ↥(periodPolynomials K w)) (ExchangeRelations.periodActionRestrict hw ⋯) = ↑((ArithmeticFunction.sigma (w + 1)) n) - ∑ p ∈ n.divisorsAntidiagonal, ↑(min p.1 p.2) ^ (w + 1) - ∑ t ∈ Finset.Icc (-4 * ↑n) (4 * ↑n) with t ^ 2 ≤ 4 * ↑n, ↑(hurwitzClassNumber (4 * ↑n - t ^ 2).toNat) * Polynomial.eval (↑t) (Polynomial.dickson 2 (↑n) w)

The class-number trace formula on period polynomials. For positive even degree w, Popa–Zagier's explicit Hecke element has trace σ_{w+1}(n) minus the divisor-minimum sum and the Hurwitz-class-number sum, whose weight P_{w+2}(t,n) in Popa–Zagier's indexing is (dickson 2 n w).eval t. The discriminant-zero terms use H(0) = -1/12. This is the trace on the full space W_w, before the Eichler–Shimura transfer to cusp forms.