By the definition of the Fourier transform, the left-hand side expands as

while the right-hand side expands as

Since

the claim then follows from Fubini’s theorem.

The left-hand side expands as

so by Fubini’s theorem it suffices to verify the identity

From two integration by parts we obtain the identity

Now apply the triangle inequality and the identity \(\int _{\bf R} \frac{dt}{1+t^2}\ dt = \pi \) to obtain the claim with \(C = \pi + 1 / 4 \pi \).

By the preceding two lemmas, we know that for any \(\sigma {\gt}1\), we have

Now take limits as \(\sigma \to 1\) using dominated convergence together with 1 and Lemma 3 to obtain the result.

Immediate from the Riemann-Lebesgue lemma, and also noting that \(\int _{-\infty }^{-\log x} \hat\psi (\frac{u}{2\pi })\ du = o(1)\).

A standard analysis lemma, which can be proven by convolving \(1_K\) with a smooth approximation to the identity for some interval \(K\) between \(I\) and \(J\). Note that we have “SmoothBumpFunction”s on smooth manifolds in Mathlib, so this shouldn’t be too hard...

For any \(R{\gt}1\), one can use a smooth cutoff function (provided by Lemma 5 to write \(\psi = \psi _{\leq R} + \psi _{{\gt}R}\), where \(\psi _{\leq R}\) is \(C^2\) (in fact smooth) and compactly supported (on \([-R,R]\)), and \(\psi _{{\gt}R}\) obeys bounds of the form

where the implied constants depend on \(\psi \). By Lemma 3 we then have

Using this and 1 one can show that

(with implied constants also depending on \(A\)), while from Lemma 1 one has

Combining the two estimates and letting \(R\) be large, we obtain the claim.

This is a standard result in Fourier analysis. It can be proved here by appealing to Mellin inversion, Theorem 5. In particular, given \(f\) in the Schwartz class, let \(F : \mathbb {R}_+ \to \mathbb {C}: x \mapsto f(\log x)\) be a function in the “Mellin space”; then the Mellin transform of \(F\) on the imaginary axis \(s=it\) is the Fourier transform of \(f\). The Mellin inversion theorem gives Fourier inversion.

By Lemma 7, we can write

for all \(y{\gt}0\) and some Schwartz function \(\psi \). Making this substitution, the claim is then equivalent after standard manipulations to

and the claim follows from Lemma 6.

Use Lemma 5 to bound \(1_I\) above and below by smooth compactly supported functions whose integral is close to the measure of \(|I|\), and use the non-negativity of \(f\).

Apply the preceding proposition with \(I = [\varepsilon ,1]\) and then send \(\varepsilon \) to zero (using 1 to control the error).

Already done by Stoll, assuming Wiener-Ikehara.

Repeat the proof of Lemma reflimiting-variant, but use monotone convergence instead of dominated convergence. (The proof should be simpler, as one no longer needs to establish domination for the sum.)

For \(x \geq 1\), this readily follows from the previous lemma and the triangle inequality. For \(x {\lt} 1\), only a bounded number of summands can contribute and the claim is trivial.

For \(x \geq 1\) apply the previous corollary for all \(y {\lt} C x\) and \(\psi \) chosen be both nonnegative and have nonnegative Fourier transform, while being not identically zero, and \(C\) a large constant. This gives

But observe that the quantity \(\int _0^{Cx} \hat\psi ( \frac{1}{2\pi }\) is non-negative and equal to the positive constant \(\int _{{\bf R}} \hat\psi ( \frac{1}{2\pi } u ) e^u\ du\) if \(n \leq x\) and \(C\) is large enough. The claim follows.

Use Corollary 5 to remove the Chebyshev hypothesis in Theorem 3.

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

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

Combining these two facts, we obtain the claim.

We expand out the left-hand side using Lemma 9. 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

also extends continuously here. But we already know that

extends, and from Euler product machinery one has the identity

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

Apply Theorem 3 (or Theorem 6) to Proposition 2. (The Chebyshev bound follows from the corresponding bound for \(\Lambda \).)