def DirichletPrimesAP.pi_count (N : ℕ) : ℕ

The prime-counting function π(N) = #{p ≤ N : p prime}.

def DirichletPrimesAP.pi_count_mod (N q a : ℕ) : ℕ

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

def DirichletPrimesAP.coprimeResidues (q : ℕ) : Finset ℕ

The set of residues a ∈ {0, …, q − 1} coprime to q, i.e. (ℤ/qℤ)ˣ.

noncomputable def DirichletPrimesAP.delta_q (q N : ℕ) : ℝ

The discrepancy Δ_q(N) = max_{a ∈ (ℤ/qℤ)ˣ} |π(N; q, a) − π(N)/φ(q)| measuring how far primes up to N are from being equidistributed among the reduced residue classes modulo q.

theorem DirichletPrimesAP.dirichlet_primes_in_ap (q : ℕ) (hq : q ≠ 0) : Filter.Tendsto (fun (N : ℕ) => delta_q q N / (↑N / ↑q)) Filter.atTop (nhds 0)

Dirichlet's theorem on primes in arithmetic progressions (quantitative form): for every q ≠ 0, the discrepancy Δ_q(N) is o(N/q) as N → ∞, i.e. Δ_q(N) / (N/q) → 0. This is the asymptotic equidistribution of primes among reduced residue classes modulo q.