Ramanujan–Petersson for cusp forms of weight $k\ge2$ (Deligne 1971/1974)

Open

RamanujanPetersson.petersson_weight_ge_two

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 (it contains $\Gamma(N)$ for some $N\ge1$ ), let $k\ge 2$ be an integer, and let $f$ be a holomorphic cusp form of weight $k$ 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^{(k-1)/2+\varepsilon}\right).

This is the case of the Ramanujan–Petersson conjecture that Deligne reduced to the Weil conjectures via the Eichler–Shimura isomorphism, and then proved.

Formalization Note $\Gamma$ is mapped into $GL(2,\mathbb R)$ , $f$ is a Mathlib CuspForm, and $a_n$ is the $n$ -th coefficient of qExpansion with period $h=$ strictWidthInfty of $\Gamma$ , which equals $1$ when $z\mapsto z+1$ lies in $\Gamma$ .

Preamble

import Mathlib

open UpperHalfPlane Filter Asymptotics MatrixGroups

Formal statement

namespace RamanujanPetersson

theorem petersson_weight_ge_two (Γ : Subgroup SL(2, ℤ))
    (hΓ : CongruenceSubgroup.IsCongruenceSubgroup Γ) (k : ℤ) (hk : 2 ≤ k)
    (f : CuspForm (Γ : Subgroup (GL (Fin 2) ℝ)) k) (ε : ℝ) (hε : 0 < ε) :
    (fun n : ℕ => (qExpansion (Γ : Subgroup (GL (Fin 2) ℝ)).strictWidthInfty f).coeff n)
      =O[atTop] fun n : ℕ => (n : ℝ) ^ (((k : ℝ) - 1) / 2 + ε) := 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": statement

a_n=O(n^{(k-1)/2+\epsilon})

for holomorphic cusp forms for congruence subgroups, and "Deligne (1971) used the Eichler–Shimura isomorphism to reduce this conjecture to the Weil conjectures that he later proved"

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 k≥2k\ge2k≥2 (Deligne 1971/1974)

Ramanujan–Petersson for cusp forms of weight $k\ge2$ (Deligne 1971/1974)