Prime number theorem for arithmetic progressions

DefinitionPrime counting in a residue class#✓fully proved

For natural numbers \(X\), \(q\) and \(a\), \(\pi(X; q, a)\) is the number of primes \(p \le X\) with \(p \equiv a \pmod q\). The modulus \(q = 1\) is allowed, and for \(q = 0\) the congruence means \(p = a\).

def primeCountingMod (X q a : ℕ) : ℕ :=
  ((X.primesLE.filter fun p => p ≡ a [MOD q]).card)

Used by 7

Used byBrun–Titchmarsh inequality · Uniform Brun–Titchmarsh bound · The set where primes \(\equiv 3 \pmod 4\) lead · Hardy–Littlewood sign changes in the prime race modulo 4 · Residue-class prime count as a filtered range · Prime counting modulo one · Prime number theorem for the residue-class prime count

TheoremPrime counting modulo one#✓fully proved

For all natural numbers \(X\) and \(a\), the number \(\pi(X; 1, a)\) of primes \(p \le X\) with \(p \equiv a \pmod 1\) equals \(\pi(X)\), the number of primes \(p \le X\).

Modulus one imposes no residue condition.

theorem primeCountingMod_one (X a : ℕ) :
    primeCountingMod X 1 a = Nat.primeCounting X

Uses 1

Statement usesPrime counting in a residue class

TheoremResidue-class prime count as a filtered range#✓fully proved

For all natural numbers \(n\), \(q\) and \(a\), the number \(\pi(n; q, a)\) of primes \(p \le n\) with \(p \equiv a \pmod q\) equals the number of integers \(p\) with \(0 \le p \le n\) such that \(p\) is prime and \(p \equiv a \pmod q\).

theorem primeCountingMod_eq_card_filter_range (n q a : ℕ) :
    Nat.primeCountingMod n q a
      = ((Finset.range (n + 1)).filter
        fun p => Nat.Prime p ∧ Nat.ModEq q p a).card

Uses 1 · Used by 3

Statement usesPrime counting in a residue class

Used byBrun–Titchmarsh inequality · Uniform Brun–Titchmarsh bound · Prime number theorem for the residue-class prime count

DefinitionChebyshev's function in a residue class#✓fully proved

For a natural number \(q\), a residue class \(a \in \mathbb{Z}/q\mathbb{Z}\) and a real number \(x\), \(\psi(x; q, a)\) is the sum of the von Mangoldt function \(\Lambda(n)\) over the positive integers \(n \le x\) with \(n \equiv a \pmod q\).

noncomputable def psiResidueClass {q : ℕ} (a : ZMod q) (x : ℝ) : ℝ :=
  ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, ArithmeticFunction.vonMangoldt.residueClass a n

Used by 8

Used byResidue-class error of Chebyshev's function · Mertens' theorem in arithmetic progressions · Prime number theorem in arithmetic progressions · The residue-class Chebyshev function vanishes below one · Prime number theorem for Chebyshev's function in a reduced residue class · Weak prime number theorem in arithmetic progressions · Siegel–Walfisz theorem for Chebyshev's function in residue classes · Landau–Ramanujan theorem

TheoremThe residue-class Chebyshev function vanishes below one#✓fully proved

For every natural number \(q\), every residue class \(a \in \mathbb{Z}/q\mathbb{Z}\) and every real number \(x < 1\), we have \(\psi(x; q, a) = 0\), where \(\psi(x; q, a)\) is the sum of the von Mangoldt function \(\Lambda(n)\) over the positive integers \(n \le x\) with \(n \equiv a \pmod q\).

theorem psiResidueClass_of_lt_one {q : ℕ} (a : ZMod q) {x : ℝ}
    (hx : x < 1) : psiResidueClass a x = 0

Uses 1

Statement usesChebyshev's function in a residue class

LemmaPrime number theorem for Chebyshev's function in a reduced residue class#✓fully proved

Let \(q \ge 1\) be an integer, let \(b\) be a unit of \(\mathbb{Z}/q\mathbb{Z}\), let \(\Lambda\) be the von Mangoldt function and let \(\varphi\) be Euler's totient function. For real \(x\) let \(\psi(x; q, b)\) be the sum of \(\Lambda(n)\) over the integers \(1 \le n \le x\) with \(n \equiv b \pmod{q}\). Then \(\psi(x; q, b)/x \to 1/\varphi(q)\) as the real number \(x\) tends to infinity.

public lemma tendsto_psiResidueClass_div_self {q : ℕ} [NeZero q]
    (b : ZMod q) (hb : IsUnit b) :
    Filter.Tendsto (fun x : ℝ => psiResidueClass b x / x) Filter.atTop
      (nhds ((q.totient : ℝ)⁻¹))

Uses 7 · Used by 4

Statement usesChebyshev's function in a residue class

Proof usesIntegral criterion for asymptotic equivalence to the identity · Laplace transform with a given value · Convergence of the Laplace transform · The one-sided Laplace transform · Convergence of the Laplace transform under an exponential bound · Newman's Tauberian theorem

Used byMertens' theorem in arithmetic progressions · Prime number theorem in arithmetic progressions · Weak prime number theorem in arithmetic progressions · Landau–Ramanujan theorem

LemmaMertens' theorem in arithmetic progressions#✓fully proved

Let \(q \ge 1\) be an integer, let \(b\) be a unit of \(\mathbb{Z}/q\mathbb{Z}\), let \(\Lambda\) be the von Mangoldt function and let \(\varphi\) be Euler's totient function. There is a real constant \(C\) such that for every real \(x \ge 1\),

\[ \left| \sum_{\substack{1 \le n \le x \\ n \equiv b \pmod{q}}} \frac{\Lambda(n)}{n} - \frac{\log x}{\varphi(q)} \right| \le C. \]

public lemma exists_abs_sum_residueClass_div_sub_log_le {q : ℕ} [NeZero q]
    (b : ZMod q) (hb : IsUnit b) :
    ∃ C : ℝ, ∀ x : ℝ, 1 ≤ x →
      |(∑ n ∈ Finset.Ioc 0 ⌊x⌋₊,
        ArithmeticFunction.vonMangoldt.residueClass b n / (n : ℝ)) -
        Real.log x / (q.totient : ℝ)| ≤ C

Uses 7 · Used by 1

Proof usesChebyshev's function in a residue class · Prime number theorem for Chebyshev's function in a reduced residue class · Laplace transform with a given value · Convergence of the Laplace transform · The one-sided Laplace transform · Convergence of the Laplace transform under an exponential bound · Newman's Tauberian theorem

Used byLandau–Ramanujan theorem

TheoremWeak prime number theorem in arithmetic progressions#✓fully proved

Let \(q\) and \(a\) be natural numbers with \(a < q\) and \(\gcd(a, q) = 1\), let \(\Lambda\) be the von Mangoldt function and let \(\varphi\) be Euler's totient function. Then, as \(N \to \infty\) through the natural numbers,

\[ \frac{1}{N} \sum_{\substack{0 \le n < N \\ n \equiv a \pmod{q}}} \Lambda(n) \to \frac{1}{\varphi(q)}. \]

public theorem weakPNT_arithmeticProgression {q a : ℕ}
    (ha : Nat.Coprime a q) (ha_lt : a < q) :
    Filter.Tendsto
      (fun N : ℕ =>
        (∑ n ∈ Finset.range N,
            if n % q = a then ArithmeticFunction.vonMangoldt n else 0) / (N : ℝ))
      Filter.atTop (nhds (1 / (Nat.totient q : ℝ)))

Sources

• the proved theorem PrimeNumberTheoremAnd.WeakPNT_AP in PrimeNumberTheoremAnd, and its use in arXiv:2608.24035. Lean preserves the source's natural representative and half-open Finset.range normalization, while omitting the redundant assumption 1 ≤ q, which follows from a < q.

Uses 2

Proof usesChebyshev's function in a residue class · Prime number theorem for Chebyshev's function in a reduced residue class

TheoremPrime number theorem in arithmetic progressions#✓fully proved

Let \(q \ge 2\) and \(a\) be natural numbers with \(\gcd(a, q) = 1\), and for each natural number \(n\) let \(N(n)\) be the number of primes \(p \le n\) with \(p \equiv a \pmod q\). Then \(N(n) \log n / n \to 1 / \varphi(q)\) as \(n \to \infty\), where \(\varphi\) is Euler's totient function and \(\log\) is the natural logarithm.

public theorem prime_number_theorem_arithmetic_progression :
    ∀ (q a : ℕ), 2 ≤ q → Nat.Coprime a q →
      Filter.Tendsto
        (fun n : ℕ =>
          (((Finset.range (n + 1)).filter fun p => Nat.Prime p ∧ Nat.ModEq q p a).card : ℝ) *
            Real.log (n : ℝ) / (n : ℝ))
        Filter.atTop (nhds (1 / (Nat.totient q : ℝ)))

Sources

• G. L. Dirichlet 1837 existence, PNT for AP by de la Vallée Poussin and Hadamard 1896-1899 extensions; textbook in Montgomery-Vaughan, Multiplicative Number Theory I, Multiplicative Number Theory

Uses 3 · Used by 1

Proof usesPrime counting versus theta over log · Chebyshev's function in a residue class · Prime number theorem for Chebyshev's function in a reduced residue class

Used byPrime number theorem for the residue-class prime count

TheoremPrime number theorem for the residue-class prime count#✓fully proved

Let \(q \ge 2\) and \(a\) be natural numbers with \(\gcd(a, q) = 1\), and let \(\pi(n; q, a)\) be the number of primes \(p \le n\) with \(p \equiv a \pmod q\). Then \(\pi(n; q, a) \log n / n \to 1 / \varphi(q)\) as \(n \to \infty\), where \(\varphi\) is Euler's totient function and \(\log\) is the natural logarithm.

public theorem tendsto_primeCountingMod_mul_log_div (q a : ℕ)
    (hq : 2 ≤ q) (hcop : Nat.Coprime a q) :
    Filter.Tendsto
      (fun n : ℕ =>
        (Nat.primeCountingMod n q a : ℝ) * Real.log (n : ℝ) / (n : ℝ))
      Filter.atTop (nhds (1 / (Nat.totient q : ℝ)))

Uses 3

Statement usesPrime counting in a residue class

Proof usesPrime number theorem in arithmetic progressions · Residue-class prime count as a filtered range

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.