Divisor bound $|\tau(n)|\le d(n)\,n^{11/2}$

Open

RamanujanPetersson.tau_le_card_divisors_mul

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

modular-formsnumber-theory

For every integer $n\ge1$ ,

|\tau(n)|\le d(n)\,n^{11/2},

where $d(n)$ is the number of positive divisors of $n$ .

As noted by Ramanujan, this follows from his three conjectures. It extends the prime bound to all $n$ .

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

Preamble

import Mathlib
import Definitions.Def_RamanujanPetersson_tau

open UpperHalfPlane Filter Asymptotics MatrixGroups
open scoped Real

Formal statement

namespace RamanujanPetersson

theorem tau_le_card_divisors_mul :
    ∀ n : ℕ, 1 ≤ n → ‖tau n‖ ≤ (n.divisors.card : ℝ) * (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", paragraph after conjecture 3 ("these conjectures imply that

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

for all

n\ge1

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

Divisor bound ∣τ(n)∣≤d(n) n11/2|\tau(n)|\le d(n)\,n^{11/2}∣τ(n)∣≤d(n)n11/2

Divisor bound $|\tau(n)|\le d(n)\,n^{11/2}$