Ramanujan's bound $|\tau(p)|\le 2p^{11/2}$ (Deligne 1974)

Open

RamanujanPetersson.tau_prime_bound

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

modular-formsnumber-theory

For every prime $p$ ,

|\tau(p)|\le 2\,p^{11/2}.

This is the third of Ramanujan's 1916 conjectures. It is equivalent to the statement that the polynomial $1-\tau(p)u+p^{11}u^2$ has non-real or double roots, and it follows from Deligne's proof (1974) of the Riemann hypothesis for varieties over finite fields.

Formalization Note $\tau$ is RamanujanPetersson.tau, the $n$ -th coefficient of Mathlib's $q$ -expansion (period $1$ ) of ModularForm.discriminant, valued in $\mathbb C$ .

Preamble

import Mathlib
import Definitions.Def_RamanujanPetersson_tau

open UpperHalfPlane Filter Asymptotics MatrixGroups
open scoped Real

Formal statement

namespace RamanujanPetersson

theorem tau_prime_bound :
    ∀ p : ℕ, p.Prime → ‖tau p‖ ≤ 2 * (p : ℝ) ^ ((11 : ℝ) / 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 conjecture", Ramanujan's conjecture 3 ("

|\tau(p)|\le 2p^{11/2}

for all primes

p

"); proved via Deligne (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's bound ∣τ(p)∣≤2p11/2|\tau(p)|\le 2p^{11/2}∣τ(p)∣≤2p11/2 (Deligne 1974)

Ramanujan's bound $|\tau(p)|\le 2p^{11/2}$ (Deligne 1974)