$\tau(n)=O(n^{11/2+\varepsilon})$

Open

RamanujanPetersson.tau_isBigO

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

modular-formsnumber-theory

For every $\varepsilon>0$ there is a constant $C_\varepsilon$ such that, for all sufficiently large $n$ ,

|\tau(n)|\le C_\varepsilon\, n^{11/2+\varepsilon},

that is, $\tau(n)=O(n^{11/2+\varepsilon})$ . This is the Ramanujan–Petersson bound for $\Delta$ (weight $12$ ), and it is a special case of the mission goal.

Formalization Note $\tau$ is RamanujanPetersson.tau, the $n$ -th coefficient of Mathlib's $q$ -expansion (period $1$ ) of ModularForm.discriminant, valued in $\mathbb C$ . The bound is Mathlib's big-O along atTop on $\mathbb N$ .

Preamble

import Mathlib
import Definitions.Def_RamanujanPetersson_tau

open UpperHalfPlane Filter Asymptotics MatrixGroups
open scoped Real

Formal statement

namespace RamanujanPetersson

theorem tau_isBigO (ε : ℝ) (hε : 0 < ε) :
    (fun n : ℕ => tau n) =O[atTop] fun n : ℕ => (n : ℝ) ^ ((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", display "A classic bound on

d(n)

thus yields

\tau(n)=O(n^{11/2+\epsilon})

"; also section "Ramanujan L-function" ("this estimate was proven unconditionally")

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

τ(n)=O(n11/2+ε)\tau(n)=O(n^{11/2+\varepsilon})τ(n)=O(n11/2+ε)

$\tau(n)=O(n^{11/2+\varepsilon})$