noncomputable def SiegelWalfisz.primeCountingArithProg (N q a : ℕ) : ℕ

The prime counting function for an arithmetic progression: the number of primes $p \le N$ with $p \equiv a \pmod{q}$.

theorem SiegelWalfisz.siegel_walfisz (A : ℝ) (hA : A > 0) : ∃ c_A > 0, ∀ (N q a : ℕ), a.Coprime q → |↑(primeCountingArithProg N q a) - ↑N.primeCounting / ↑q.totient| ≤ c_A * ↑N * Real.log ↑N ^ (-A)

Siegel--Walfisz theorem. For every $A > 0$ there is a constant $c_A > 0$ such that for all coprime $a, q$, the discrepancy $\Delta_q(N)$ between the number of primes $\le N$ in the residue class $a \pmod q$ and the expected value $\pi(N)/\varphi(q)$ satisfies $\Delta_q(N) \le c_A N (\log N)^{-A}$.