The prime number theorem in arithmetic progressions

LemmaWeakPNT-character#

If \(q ≥ 1\) and \(a\) is coprime to \(q\), and \(\mathrm{Re} s > 1\), we have

\[ \sum_{n: n = a\ (q)} \frac{\Lambda(n)}{n^s} = - \frac{1}{\varphi(q)} \sum_{\chi\ (q)} \overline{\chi(a)} \frac{L'(s,\chi)}{L(s,\chi)}. \]
Proof

From the Fourier inversion formula on the multiplicative group \((\mathbb{Z}/q\mathbb{Z})^\times\), we have

\[ 1_{n=a\ (q)} = \frac{\varphi(q)}{q} \sum_{\chi\ (q)} \overline{\chi(a)} \chi(n). \]

On the other hand, from standard facts about L-series we have for each character \(\chi\) that

\[ \sum_{n} \frac{\Lambda(n) \chi(n)}{n^s} = - \frac{L'(s,\chi)}{L(s,\chi)}. \]

Combining these two facts, we obtain the claim.

Lean

Formalized as WeakPNT_character.

Sources
LeanWeakPNT_character
Used by 1
Used byWeakPNT-AP-prelim

PropositionWeakPNT-AP-prelim#

If \(q ≥ 1\) and \(a\) is coprime to \(q\), the Dirichlet series \(\sum_{n \leq x: n = a\ (q)} \frac{\Lambda(n)}{n^s}\) converges for \(\mathrm{Re}(s) > 1\) to \(\frac{1}{\varphi(q)} \frac{1}{s-1} + G(s)\) where \(G\) has a continuous extension to \(\mathrm{Re}(s)=1\).

Proof

We expand out the left-hand side using Lemma WeakPNT-character. The contribution of the non-principal characters \(\chi\) extend continuously to \(\mathrm{Re}(s) = 1\) thanks to the non-vanishing of \(L(s,\chi)\) on this line (which should follow from another component of this project), so it suffices to show that for the principal character \(\chi_0\), that

\[ -\frac{L'(s,\chi_0)}{L(s,\chi_0)} - \frac{1}{s-1} \]

also extends continuously here. But we already know that

\[ -\frac{\zeta'(s)}{\zeta(s)} - \frac{1}{s-1} \]

extends, and from Euler product machinery one has the identity

\[ \frac{L'(s,\chi_0)}{L(s,\chi_0)} = \frac{\zeta'(s)}{\zeta(s)} + \sum_{p|q} \frac{\log p}{p^s-1}. \]

Since there are only finitely many primes dividing \(q\), and each summand \(\frac{\log p}{p^s-1}\) extends continuously, the claim follows.

Lean

Formalized as WeakPNT_AP_prelim.

Sources
LeanWeakPNT_AP_prelim
Uses 2 · Used by 1
Proof usesChebyshevPsi · WeakPNT-character
Used byWeakPNT-AP

TheoremWeakPNT-AP#

If \(q ≥ 1\) and \(a\) is coprime to \(q\), we have

\[ \sum_{n \leq x: n = a\ (q)} \Lambda(n) = \frac{x}{\varphi(q)} + o(x). \]
Proof

Apply Theorem Wiener-Ikehara Theorem (1) (or Theorem Wiener-Ikehara Theorem (2) to avoid checking the Chebyshev condition) using Proposition WeakPNT-AP-prelim.

Lean

Formalized as WeakPNT_AP.

Sources
LeanWeakPNT_AP
Uses 3 · Used by 1
Proof usesWiener-Ikehara Theorem (2) · WeakPNT-AP-prelim · Wiener-Ikehara Theorem (1)
Used byPrime number theorem in AP

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.