Rademacher's convexity bound for primitive Dirichlet $L$ -functions

Proved

QRHLittlewood.rademacher_convexity

by @bwdaugherty · 1 vote · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorynumber-theory

Let $\chi$ be a primitive Dirichlet character modulo $q\ge3$ and let $s$ be a complex number with $-\tfrac12\le\Re s\le\tfrac32$ . Then

|L(s,\chi)|\ \le\ \zeta\big(\tfrac32\big)\left(\frac{q\,|1+s|}{2\pi}\right)^{(3/2-\Re s)/2}.

It interpolates between the trivial bound $|L(s,\chi)|\le\zeta(3/2)$ on $\Re s=3/2$ and the bound on $\Re s=-1/2$ given by the functional equation.

Preamble

import Mathlib.NumberTheory.Harmonic.EulerMascheroni
import Mathlib.NumberTheory.LSeries.DirichletContinuation

open Real

Formal statement

namespace QRHLittlewood

theorem rademacher_convexity (q : ℕ) [NeZero q] (hq : 3 ≤ q) (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive)
    (s : ℂ) (hs1 : -1 / 2 ≤ s.re) (hs2 : s.re ≤ 3 / 2) :
    ‖DirichletCharacter.LFunction χ s‖ ≤
      (riemannZeta (3 / 2)).re * ((q : ℝ) * ‖1 + s‖ / (2 * π)) ^ ((3 / 2 - s.re) / 2) := by sorry

end QRHLittlewood

Source

H. Rademacher, On the Phragmén–Lindelöf theorem and some applications, Math. Z. 72 (1959/60), 192–204 (exponent 1/2 case); as stated and used in B. W. Daugherty, S. Ryan, G. Ward, Certified harmonic-measure barriers and explicit Littlewood bounds from zero-free regions, https://doi.org/10.5281/zenodo.23400116, Section 6, "The Dirichlet inputs".

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Statement. Let $q$ be a natural number with $q\neq0$ and $q\ge 3$ . Let $\chi$ be a primitive $\mathbb{C}$ -valued Dirichlet character modulo $q$ (conductor exactly $q$ ). Let $s\in\mathbb{C}$ with

-\tfrac12\le\operatorname{Re}s\le\tfrac32 .

Then

|L(s,\chi)|\;\le\;\zeta\!\left(\tfrac32\right)\left(\frac{q\,|1+s|}{2\pi}\right)^{\frac{3/2-\operatorname{Re}s}{2}},

where $|\cdot|$ is the complex modulus and $\zeta(3/2)\approx 2.612$ enters as the real part of Mathlib's $\zeta(3/2)$ (which is real).

Here $L(s,\chi)$ is Mathlib's Dirichlet $L$ -function: the unique meromorphic continuation to all of $\mathbb{C}$ of $\sum_{n\ge1}\chi(n)n^{-s}$ (built from Hurwitz zeta functions); it is a total function $\mathbb{C}\to\mathbb{C}$ , and at a pole (only possible at $s=1$ for the trivial character) it returns a fixed finite junk value. "Primitive" means the conductor of $\chi$ (the least $d\mid q$ through which $\chi$ factors) equals $q$ . "Real-valued" means $\operatorname{Im}\chi(a)=0$ for every residue class $a\in\mathbb{Z}/q\mathbb{Z}$ , including non-units (where $\chi(a)=0$ anyway).

Edge cases and scope.

No reality assumption on $\chi$ : the statement covers every primitive character modulo $q\ge3$ , both even and odd, real or complex.
Since $q\ge3$ and $\chi$ is primitive, $\chi$ is nontrivial, so $L(s,\chi)$ is entire and the value at $s=1$ (which lies in the strip) is genuine.
The base $q|1+s|/(2\pi)$ is a nonnegative real; since $\operatorname{Re}(1+s)\ge\frac12$ , it is strictly positive. The exponent $(3/2-\operatorname{Re}s)/2$ lies in $[0,1]$ ; it equals $0$ at $\operatorname{Re}s=3/2$ , where the bound reads $|L(s,\chi)|\le\zeta(3/2)$ , and equals $1$ at $\operatorname{Re}s=-\tfrac12$ .
The bound uses $|1+s|$ (not $|s|$ or $|s|+1$ ) and the closed strip, both endpoints included. There is no zero-free or other analytic hypothesis.

Human review

Endorsed by Shuze Chen · Oct 16, 2026
Confirmed by the moderator at approval.
Endorsed by @bwdaugherty · Oct 16, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Rademacher's convexity bound for primitive Dirichlet LLL-functions

Rademacher's convexity bound for primitive Dirichlet $L$ -functions