Logarithmically weighted square summability of cusp-form coefficients

Proved

MTT.cusp_log_weighted_square_summable

by davidloeffler · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

group-cohomologymodular-forms

For a weight- $k$ cusp form $f$ on $\Gamma_1(N)$ , with $N>0$ and $k\ge2$ , its width-one Fourier coefficients satisfy

\sum_{m\ge1}\frac{|a_m(f)|^2\log m}{m^{k+1}}<\infty.

This includes weight 2. The term at $m=0$ in the Lean sum is zero by the totalized logarithm and division conventions. The coefficients are the actual coefficients of the analytic q-expansion.

Preamble

import Definitions.Def_MTT_Cohomology_Boundary
import Mathlib.NumberTheory.LSeries.PrimesInAP
set_option autoImplicit false
noncomputable section
open scoped BigOperators
open MTT.Cohomology

Formal statement

theorem MTT.cusp_log_weighted_square_summable
    {N k : ℕ} (hN : 0 < N) (hk : 2 ≤ k)
    (f : CuspForm (MTT.GammaOne N) (k : ℤ)) :
    Summable (fun m : ℕ =>
      ‖(UpperHalfPlane.qExpansion 1 f).coeff m‖^2 * Real.log m /
        (m : ℝ)^(k+1)) := by sorry

Source

Z. Rudnick, Modular forms 2019: Petersson formula notes, Lemma 1.1 and Theorem 1.2, pp. 2–3, https://www.math.tau.ac.il/~rudnick/courses/modular%20forms%202019/peterssonformula.pdf. The Parseval estimate sum_{m≤X}|a_m|² ≪ X^k gives the stated summability by dyadic summation; finite-index congruence level uses the same argument.

View graph