Ramanujan–Petersson for cusp forms of weight $1$ (Deligne–Serre 1974)

Open

RamanujanPetersson.petersson_weight_one

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

modular-formsnumber-theory

Let $\Gamma\subseteq SL(2,\mathbb Z)$ be a congruence subgroup and let $f$ be a holomorphic cusp form of weight $1$ for $\Gamma$ . Let $h>0$ be the width of the cusp $\infty$ for $\Gamma$ and write $f(z)=\sum_{n\ge0}a_n e^{2\pi i n z/h}$ . Then for every $\varepsilon>0$ ,

a_n=O_\varepsilon\!\left(n^{\varepsilon}\right),

which is the bound $n^{(k-1)/2+\varepsilon}$ for $k=1$ .

This weight-one case is due to Deligne and Serre.

Formalization Note Same conventions as the weight $k\ge2$ milestone: Mathlib CuspForm for the image of $\Gamma$ in $GL(2,\mathbb R)$ , coefficients from qExpansion with period strictWidthInfty.

Preamble

import Mathlib

open UpperHalfPlane Filter Asymptotics MatrixGroups

Formal statement

namespace RamanujanPetersson

theorem petersson_weight_one (Γ : Subgroup SL(2, ℤ))
    (hΓ : CongruenceSubgroup.IsCongruenceSubgroup Γ)
    (f : CuspForm (Γ : Subgroup (GL (Fin 2) ℝ)) 1) (ε : ℝ) (hε : 0 < ε) :
    (fun n : ℕ => (qExpansion (Γ : Subgroup (GL (Fin 2) ℝ)).strictWidthInfty f).coeff n)
      =O[atTop] fun n : ℕ => (n : ℝ) ^ ε := by sorry

end RamanujanPetersson

Source

Wikipedia, "Ramanujan–Petersson conjecture", https://en.wikipedia.org/w/index.php?title=Ramanujan%E2%80%93Petersson_conjecture&oldid=1369029052 (PDF snapshot supplied by the proposer, 9 pp.), section "Ramanujan–Petersson conjecture for modular forms": "This is also true for the case

k=1

, where it is a result of Deligne & Serre (1974)"

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Ramanujan–Petersson for cusp forms of weight 111 (Deligne–Serre 1974)

Ramanujan–Petersson for cusp forms of weight $1$ (Deligne–Serre 1974)