Removing the Chebyshev hypothesis

In this section we do *not* assume the bound (1), but instead derive it from the other hypotheses.

Lemmalimiting-fourier-variant #

If \(\psi: \mathbb{R} \to \mathbb{C}\) is \(C^2\) and compactly supported with \(f\) and \(\hat \psi\) non-negative, and \(0 < x\), then

\[ \sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} ) - A \int_{-\log x}^\infty \hat \psi(\frac{u}{2\pi})\ du = \int_\mathbb{R} G(1+it) \psi(t) x^{it}\ dt. \]

Proof

Repeat the proof of Lemma limiting-fourier-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.)

Lean

Formalized as limiting_fourier_variant.

Sources

PNT+ blueprint: PrimeNumberTheoremAnd/Wiener.lean

Leanlimiting_fourier_variant

Uses 3 · Used by 1

Proof usessecond-fourier · first-fourier · Decay bounds

Used bycrude-upper-bound

Corollarycrude-upper-bound #

If \(\psi: \mathbb{R} \to \mathbb{C}\) is \(C^2\) and compactly supported with \(f\) and \(\hat \psi\) non-negative, then there exists a constant \(B\) such that

\[ |\sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} )| \leq B \]

for all \(x > 0\).

Proof

This readily follows from the previous lemma and the triangle inequality.

Lean

Formalized as crude_upper_bound.

Sources

PNT+ blueprint: PrimeNumberTheoremAnd/Wiener.lean

Leancrude_upper_bound

Uses 1 · Used by 1

Proof useslimiting-fourier-variant

Used byauto-cheby

Corollaryauto-cheby #

One has

\[ \sum_{n \leq x} f(n) = O(x) \]

for all \(x \geq 1\).

Proof

By applying Corollary crude-upper-bound for a specific compactly supported function \(\psi\), one can obtain a bound of the form \(\sum_{(1-\varepsilon)x < n \leq x} f(n) = O(x)\) for all \(x\) and some absolute constant \(\varepsilon\) (which can be made explicit).

If \(C\) is a sufficiently large constant, the claim \(|\sum_{n \leq x} f(n)| \leq Cx\) can now be proven by strong induction on \(x\), as the claim for \((1-\varepsilon)x\) implies the claim for \(x\) by the triangle inequality (and the claim is trivial for \(x < 1\)).