The Siegel–Walfisz theorem for arithmetic progressions (Davenport §22)

Proved

Davenport.siegel_walfisz_ap

by alya · Sep 3, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theorydirichlet-l-functionnumber-theorysiegel-walfiszthree-primes

The Siegel–Walfisz theorem, progression form (Davenport §22). For any fixed $A>0$ there are constants $c,C>0$ such that for all $N\ge2$ , all moduli $1\le q\le(\log N)^A$ and all $a$ with $\gcd(a,q)=1$ ,

\Bigl|\psi(N;q,a)-\frac{N}{\varphi(q)}\Bigr|\;\le\;C\,N\exp\bigl(-c\sqrt{\log N}\bigr),\qquad \psi(N;q,a)=\sum_{\substack{n<N\\ n\equiv a\ (q)}}\Lambda(n),

i.e. $\psi(x;q,a)=x/\varphi(q)+O\bigl(x\exp(-C_A(\log x)^{1/2})\bigr)$ uniformly for $q\le(\log x)^A$ . It follows from the character form by orthogonality of characters, $\psi(N;q,a)=\varphi(q)^{-1}\sum_{\chi}\overline{\chi}(a)\psi(N,\chi)$ . The constants are ineffective.

Preamble

import Definitions.Def_Davenport_siegelWalfisz
import Mathlib.NumberTheory.LSeries.DirichletContinuation
import Mathlib.NumberTheory.DirichletCharacter.Basic
import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
import Mathlib.NumberTheory.Chebyshev
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Pow.Complex
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Algebra.BigOperators.Finprod
import Mathlib.Data.Nat.Totient

open Finset DirichletCharacter Vino

Formal statement

namespace Davenport

theorem siegel_walfisz_ap (A : ℝ) (hA : 0 < A) :
    ∃ c C : ℝ, 0 < c ∧ 0 < C ∧
      ∀ (N q a : ℕ), 2 ≤ N → 1 ≤ q → (q : ℝ) ≤ Real.log N ^ A → Nat.Coprime a q →
        |psiAP N q a - (N : ℝ) / (Nat.totient q : ℝ)|
          ≤ C * N * Real.exp (-c * Real.sqrt (Real.log N)) := by sorry

end Davenport

Source

H. Davenport, Multiplicative Number Theory, 3rd ed. (revised by H. L. Montgomery), GTM 74, Springer, 2000, https://doi.org/10.1007/978-1-4757-5927-3; §22 (The prime number theorem for arithmetic progressions (II)), pp. 132–134: ψ(x;q,a) = x/φ(q) + O(x exp(−C_N (log x)^{1/2})) uniformly for q ≤ (log x)^N, (a,q) = 1

Read-back

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

Read-back: `Davenport.siegel_walfisz_ap`

Statement. For every real number $A$ satisfying $A > 0$ , there exist real numbers $c$ and $C$ with $c > 0$ and $C > 0$ , such that for all natural numbers $N$ , $q$ , $a$ satisfying the four hypotheses

$N \ge 2$ ,
$q \ge 1$ ,
$q \le (\log N)^{A}$ (the natural number $q$ cast to a real, compared against the real power $(\log N)^{A}$ , i.e. $\exp(A \log \log N)$ when $\log N > 0$ ),
$\gcd(a, q) = 1$ ,

the following inequality holds:

\left| \Psi(N; q, a) - \frac{N}{\varphi(q)} \right| \;\le\; C \cdot N \cdot \exp\!\left(-c \sqrt{\log N}\right),

where $\varphi$ is Euler's totient function and $\Psi(N; q, a)$ denotes the quantity written psiAP N q a in the code, which unfolds to

\Psi(N; q, a) \;=\; \sum_{n = 0}^{N-1} \begin{cases} \Lambda(n) & \text{if } n \equiv a \pmod{q} \\ 0 & \text{otherwise,}\end{cases}

i.e. the sum of the von Mangoldt function $\Lambda$ over those $n$ in the index range $\{0, 1, \dots, N-1\}$ whose residue class modulo $q$ equals that of $a$ . Here $\Lambda(n) = \log p$ when $n = p^{k}$ for a prime $p$ and an integer $k \ge 1$ , and $\Lambda(n) = 0$ otherwise; in particular $\Lambda(0) = \Lambda(1) = 0$ , so the terms $n = 0$ and $n = 1$ contribute nothing even when they satisfy the congruence. All arithmetic in the displayed inequality is over the reals: $\Lambda(n)$ , $N$ , and $\varphi(q)$ are cast to real numbers, $\log$ is the real natural logarithm, $\sqrt{\cdot}$ the real square root, $\exp$ the real exponential, and $|\cdot|$ the real absolute value.

Quantifier order. The order is: $A$ first, then $c$ and $C$ (which may therefore depend on $A$ but on nothing else), then $N$ , $q$ , $a$ . Thus $c$ and $C$ are uniform in $N$ , $q$ , and $a$ simultaneously: a single pair $(c, C)$ must work for every admissible triple. The statement asserts only the existence of such a pair; it gives no formula for, or bound on, $c$ or $C$ , and does not claim any relation between them.

Range and endpoint conventions. The summation index runs over $0 \le n < N$ ; the endpoint $n = N$ is excluded. The main term subtracted is $N / \varphi(q)$ with the full $N$ in the numerator (not $N - 1$ , and not a count of the summation range), and it is divided by $\varphi(q)$ rather than by anything involving $N$ or $a$ .

Degenerate and edge cases silently included.

$q = 0$ is excluded by the hypothesis $q \ge 1$ , so the division by $\varphi(q)$ is never a division by $\varphi(0) = 0$ ; for $q \ge 1$ one has $\varphi(q) \ge 1$ .
$q = 1$ is permitted. Then the ring $\mathbb{Z}/1\mathbb{Z}$ is trivial, so the congruence condition $n \equiv a \pmod{1}$ holds for every $n$ , and $\Psi(N; 1, a)$ is the full Chebyshev-type sum $\sum_{n < N} \Lambda(n)$ ; also $\varphi(1) = 1$ , so the main term is $N$ , and $\gcd(a,1) = 1$ holds for every $a$ including $a = 0$ .
No hypothesis requires $a < q$ ; $a$ is an arbitrary natural number and only its residue class modulo $q$ matters. Large values of $a$ (including $a \ge q$ , or $a$ arbitrarily larger than $N$ ) are covered, as is $a = 0$ — though $\gcd(0, q) = q$ , so $a = 0$ is admissible only when $q = 1$ .
No hypothesis relates $q$ to $N$ beyond $q \le (\log N)^{A}$ ; in particular there is no assumption $q \le N$ or $q < N$ beyond what that inequality forces, and no lower bound on $N$ other than $N \ge 2$ .
The hypotheses $q \ge 1$ and $q \le (\log N)^{A}$ together force $(\log N)^{A} \ge 1$ , hence (as $A > 0$ ) $\log N \ge 1$ , i.e. $N \ge e$ , i.e. $N \ge 3$ . Consequently the case $N = 2$ — although admitted by the hypothesis $N \ge 2$ — is vacuous: no $q$ satisfies both remaining constraints, so the theorem asserts nothing for $N = 2$ . For all $N \ge 2$ one has $\log N > 0$ , so $(\log N)^{A}$ is the ordinary positive real power and $\sqrt{\log N}$ is a genuine (positive) square root rather than the value $\sqrt{x} = 0$ that the total square-root function returns on negative inputs.
Nothing is asserted for pairs $(N, q)$ with $q > (\log N)^{A}$ : the range of moduli covered grows only like a fixed power of $\log N$ , with the power $A$ fixed before $c$ and $C$ are chosen.
The inequality is non-strict ( $\le$ ) on both the modulus bound $q \le (\log N)^{A}$ and the conclusion.

What is not said. The statement contains no reference to Dirichlet characters, $L$ -functions, exceptional zeros, or any of the other definitions in the surrounding bundle; it is purely the displayed inequality on $\Psi(N; q, a)$ . It is an existence claim over $c, C$ only, with no effectivity, no uniformity in $A$ , and no assertion about the sharpness of the exponent $\sqrt{\log N}$ .

Human review

Endorsed by Shuze Chen · Sep 3, 2026
Endorsed by alya · Sep 3, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The Siegel–Walfisz theorem for arithmetic progressions (Davenport §22)

Read-back: Davenport.siegel_walfisz_ap

Read-back: `Davenport.siegel_walfisz_ap`