Partial sums $\sum_{k\le n}\tau(k)=O(n^{13/2+\varepsilon})$

Proved

RamanujanPetersson.tau_partial_sum_isBigO

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

modular-formsnumber-theory

For every $\varepsilon>0$ ,

\sum_{k=1}^{n}\tau(k)=O\!\left(n^{13/2+\varepsilon}\right)\qquad(n\to\infty).

The source presents this as the general estimate behind the absolute convergence of the Ramanujan $L$ -series.

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_partial_sum_isBigO (ε : ℝ) (hε : 0 < ε) :
    (fun n : ℕ => ∑ k ∈ Finset.Icc 1 n, tau k) =O[atTop]
      fun n : ℕ => (n : ℝ) ^ ((13 : ℝ) / 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 L-function", display "From general estimation for tau function

\sum_{k=1}^n\tau(k)=O(n^{13/2+\epsilon})

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

Partial sums ∑k≤nτ(k)=O(n13/2+ε)\sum_{k\le n}\tau(k)=O(n^{13/2+\varepsilon})∑k≤n​τ(k)=O(n13/2+ε)

Partial sums $\sum_{k\le n}\tau(k)=O(n^{13/2+\varepsilon})$