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

• PNT+ blueprint: PrimeNumberTheoremAnd/Consequences.lean

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

• PNT+ blueprint: PrimeNumberTheoremAnd/Consequences.lean

Leandirichlet_thm

Uses 1

Proof usesPrime number theorem in AP

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.