Absolute convergence of $L(s,\tau)$ for $\operatorname{Re}s>13/2$

Proved

RamanujanPetersson.L_series_summable

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

modular-formsnumber-theory

For every complex $s$ with $\operatorname{Re}s>13/2$ , the Ramanujan $L$ -series

L(s,\tau)=\sum_{n=1}^{\infty}\frac{\tau(n)}{n^{s}}

converges absolutely.

This gives the half-plane on which $L(s,\tau)$ is defined by its Dirichlet series. It is also where the Euler product is stated.

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

Preamble

import Mathlib
import Definitions.Def_RamanujanPetersson_tau

open UpperHalfPlane Filter Asymptotics MatrixGroups
open scoped Real

Formal statement

namespace RamanujanPetersson

theorem L_series_summable (s : ℂ) (hs : 13 / 2 < s.re) :
    LSeriesSummable tau s := 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", definition

L(s,\tau)=\sum_{n\ge1}\tau(n)/n^s

and "so this series converges absolutely for

\operatorname{Re}(s)>13/2

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

Absolute convergence of L(s,τ)L(s,\tau)L(s,τ) for Re⁡s>13/2\operatorname{Re}s>13/2Res>13/2

Absolute convergence of $L(s,\tau)$ for $\operatorname{Re}s>13/2$