Consequences of the PNT in arithmetic progressions

TheoremPrime number theorem in AP#

If \(a\ (q)\) is a primitive residue class, then one has

\[ \sum_{p \leq x: p = a\ (q)} \log p = \frac{x}{\phi(q)} + o(x). \]
Proof

This is a routine modification of the proof of Theorem chebyshev-asymptotic.

Lean

Formalized as chebyshev_asymptotic_pnt.

Sources
Leanchebyshev_asymptotic_pnt
Uses 2 · Used by 1
Proof usesWeakPNT-AP · chebyshev-asymptotic
Used byDirichlet's theorem

CorollaryDirichlet's theorem#

Any primitive residue class contains an infinite number of primes.

Proof

If this were not the case, then the sum \(\sum_{p \leq x: p = a\ (q)} \log p\) would be bounded in \(x\), contradicting Theorem Prime number theorem in AP.

Lean

Formalized as dirichlet_thm.

Sources
Leandirichlet_thm
Uses 1
Proof usesPrime number theorem in AP

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.