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

The number of primes p ≤ N lying in the arithmetic progression a (mod q), i.e. π(N; q, a) = #{ p ≤ N : p prime, p ≡ a (mod q) }.

noncomputable def BombieriVinogradov.primeArithProgDiscrepancy (N q : ℕ) : ℝ

Discrepancy of the distribution of primes modulo q at scale N: Δ_q(N) = sup_{(a, q) = 1} |π(N; q, a) − π(N) / φ(q)|. It measures how far the counting function on each invertible residue class deviates from the expected value π(N)/φ(q).

theorem BombieriVinogradov.bombieri_vinogradov (ε : ℝ) (hε : 0 < ε) (A : ℝ) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ), 2 ≤ N → ∑ q ∈ Finset.range (N + 1) with ↑q ≤ ↑N ^ (1 / 2 - ε), primeArithProgDiscrepancy N q ≤ C * ↑N * Real.log ↑N ^ (-A)

The Bombieri–Vinogradov theorem (Rényi, Bombieri–Vinogradov): for every ε > 0 and A > 0, there is a constant C > 0 such that for all N ≥ 2, ∑_{q ≤ N^{1/2 − ε}} Δ_q(N) ≤ C · N · (log N)^{−A}. On average over moduli q up to roughly √N, the primes in arithmetic progressions are as equidistributed as predicted by the generalized Riemann hypothesis.