Primes in arithmetic progressions

Dirichlet density, PNT for progressions, Siegel–Walfisz, Bombieri–Vinogradov, Brun–Titchmarsh, prime races.

• Discrepancy of sequences in residue classes
• Prime number theorem for arithmetic progressions
• Bombieri–Vinogradov theorem
• Brun–Titchmarsh theorem
• Chebyshev's bias
• Siegel–Walfisz theorem
• Wallis-type prime products in residue classes

TheoremDirichlet density of primes in an arithmetic progression#✓fully proved

Let \(a\) and \(m\) be natural numbers with \(m > 0\) and \(\gcd(a, m) = 1\), and let \(\varphi\) be Euler's totient function. As the real number \(s\) tends to \(1\) from above,

\[\frac{\sum_{p \equiv a \pmod{m}} p^{-s}}{\sum_{p} p^{-s}} \to \frac{1}{\varphi(m)},\]

where both sums run over primes \(p\). That is, the primes congruent to \(a\) modulo \(m\) have relative Dirichlet density \(1/\varphi(m)\) among all primes.

theorem dirichlet_density_primes_arithmetic_progression
    (a m : ℕ) (hm : 0 < m) (hcop : Nat.Coprime a m) :
    Filter.Tendsto (fun s : ℝ =>
      (∑' (p : { p : ℕ // Nat.Prime p ∧ p ≡ a [MOD m] }), (p.val : ℝ) ^ (-s)) /
      (∑' (p : { p : ℕ // Nat.Prime p }), (p.val : ℝ) ^ (-s)))
      (nhdsWithin 1 (Set.Ioi 1)) (nhds (1 / (Nat.totient m : ℝ)))

Sources

• B. Li, S. J. Miller, T. Popescu, D. Sarnecki, and N. Wattanawanichkul, "Modeling Random Walks to Infinity on Primes in Z[sqrt(2)]", Journal of Integer Sequences 25 (2022), Article 22.6.1, TeX source, relative Dirichlet-density definition at lines 281-285 and primes-in-arithmetic- progressions statement at lines 290-292.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.