A Fourier-analytic proof of the Wiener-Ikehara theorem

The Fourier transform of an absolutely integrable function \(\psi: \mathbb{R} \to \mathbb{C}\) is defined by the formula

\[ \hat \psi(u) := \int_\mathbb{R} e(-tu) \psi(t)\ dt \]

where \(e(\theta) := e^{2\pi i \theta}\).

Let \(f: \mathbb{N} \to \mathbb{C}\) be an arithmetic function such that \(\sum_{n=1}^\infty \frac{|f(n)|}{n^\sigma} < \infty\) for all \(\sigma>1\). Then the Dirichlet series

\[ F(s) := \sum_{n=1}^\infty \frac{f(n)}{n^s} \]

is absolutely convergent for \(\sigma>1\).

Lemmafirst-fourier#

If \(\psi: \mathbb{R} \to \mathbb{C}\) is integrable and \(x > 0\), then for any \(\sigma>1\)

\[ \sum_{n=1}^\infty \frac{f(n)}{n^\sigma} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} ) = \int_\mathbb{R} F(\sigma + it) \psi(t) x^{it}\ dt. \]
Proof

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

\[ \sum_{n=1}^\infty \int_\mathbb{R} \frac{f(n)}{n^\sigma} \psi(t) e( - \frac{1}{2\pi} t \log \frac{n}{x})\ dt \]

while the right-hand side expands as

\[ \int_\mathbb{R} \sum_{n=1}^\infty \frac{f(n)}{n^{\sigma+it}} \psi(t) x^{it}\ dt. \]

Since

\[ \frac{f(n)}{n^\sigma} \psi(t) e( - \frac{1}{2\pi} t \log \frac{n}{x}) = \frac{f(n)}{n^{\sigma+it}} \psi(t) x^{it} \]

the claim then follows from Fubini's theorem.

Lean

Formalized as first_fourier.

Sources
Leanfirst_fourier
Used by 3
Used byLimiting Fourier identity · auto-cheby · limiting-fourier-variant

Lemmasecond-fourier#

If \(\psi: \mathbb{R} \to \mathbb{C}\) is absolutely integrable and \(x > 0\), then for any \(\sigma>1\)

\[ \int_{-\log x}^\infty e^{-u(\sigma-1)} \hat \psi(\frac{u}{2\pi})\ du = x^{\sigma - 1} \int_\mathbb{R} \frac{1}{\sigma+it-1} \psi(t) x^{it}\ dt. \]
Proof

The left-hand side expands as

\[ \int_{-\log x}^\infty \int_\mathbb{R} e^{-u(\sigma-1)} \psi(t) e(-\frac{tu}{2\pi})\ dt\ du \]

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

\[ \begin{aligned} \int_{-\log x}^\infty e^{-u(\sigma-1)} e(-\frac{tu}{2\pi})\ du &= \int_{-\log x}^\infty e^{(it - \sigma + 1)u}\ du \\ &= \frac{1}{it - \sigma + 1} e^{(it - \sigma + 1)u}\ \Big|_{-\log x}^\infty \\ &= x^{\sigma - 1} \frac{1}{\sigma+it-1} x^{it} \end{aligned} \]
Lean

Formalized as second_fourier.

Sources
Leansecond_fourier
Used by 3
Used byLimiting Fourier identity · auto-cheby · limiting-fourier-variant

Now let \(A \in \mathbb{C}\), and suppose that there is a continuous function \(G(s)\) defined on \(\mathrm{Re} s \geq 1\) such that \(G(s) = F(s) - \frac{A}{s-1}\) whenever \(\mathrm{Re} s > 1\). We also make the Chebyshev-type hypothesis

\[ \sum_{n \leq x} |f(n)| \ll x\qquad\text{(1)} \]

for all \(x \geq 1\) (this hypothesis is not strictly necessary, but simplifies the arguments and can be obtained fairly easily in applications).

LemmaPreliminary decay bound I#

If \(\psi:\mathbb{R} \to \mathbb{C}\) is absolutely integrable then

\[ |\hat \psi(u)| \leq \| \psi \|_1 \]

for all \(u \in \mathbb{R}\). where \(C\) is an absolute constant.

Proof

Immediate from the triangle inequality.

Lean

Formalized as prelim_decay.

Sources
Leanprelim_decay
Discussionhttps://github.com/AlexKontorovich/PrimeNumberTheoremAnd/issues/561
Used by 1
Used byDecay bound, alternate form

LemmaPreliminary decay bound II#

If \(\psi:\mathbb{R} \to \mathbb{C}\) is absolutely integrable and of bounded variation, then

\[ |\hat \psi(u)| \leq \| \psi \|_{TV} / 2\pi |u| \]

for all non-zero \(u \in \mathbb{R}\).

Proof

By Lebesgue–Stiejtes integration by parts we have

\[ 2\pi i u \hat \psi(u) = \int _\mathbb{R} e(-tu) d\psi(t) \]

and the claim then follows from the triangle inequality.

Lean

Stated as prelim_decay_2; the blueprint marks no proof of it as formalized.

Sources
Leanprelim_decay_2
Discussionhttps://github.com/AlexKontorovich/PrimeNumberTheoremAnd/issues/562
Used by 1
Used byPreliminary decay bound III

LemmaPreliminary decay bound III#

If \(\psi:\mathbb{R} \to \mathbb{C}\) is absolutely integrable, absolutely continuous, and \(\psi'\) is of bounded variation, then

\[ |\hat \psi(u)| \leq \| \psi' \|_{TV} / (2\pi |u|)^2 \]

for all non-zero \(u \in \mathbb{R}\).

Proof

Should follow from previous lemma.

Lean

Stated as prelim_decay_3; the blueprint marks no proof of it as formalized.

Sources
Leanprelim_decay_3
Discussionhttps://github.com/AlexKontorovich/PrimeNumberTheoremAnd/issues/563
Uses 1 · Used by 1
Proof usesPreliminary decay bound II
Used byDecay bound, alternate form

LemmaDecay bound, alternate form#

If \(\psi:\mathbb{R} \to \mathbb{C}\) is absolutely integrable, absolutely continuous, and \(\psi'\) is of bounded variation, then

\[ |\hat \psi(u)| \leq ( \|\psi\|_1 + \| \psi' \|_{TV} / (2\pi)^2) / (1+|u|^2) \]

for all \(u \in \mathbb{R}\).

Proof

Should follow from previous lemmas.

Lean

Formalized as decay_alt.

Sources
Leandecay_alt
Discussionhttps://github.com/AlexKontorovich/PrimeNumberTheoremAnd/issues/564
Uses 3
Proof usesPreliminary decay bound III · Decay bounds · Preliminary decay bound I

LemmaDecay bounds#

If \(\psi:\mathbb{R} \to \mathbb{C}\) is \(C^2\) and obeys the bounds

\[ |\psi(t)|, |\psi''(t)| \leq A / (1 + |t|^2) \]

for all \(t \in \mathbb{R}\), then

\[ |\hat \psi(u)| \leq C A / (1+|u|^2) \]

for all \(u \in \mathbb{R}\), where \(C\) is an absolute constant.

Proof

From two integration by parts we obtain the identity

\[ (1+u^2) \hat \psi(u) = \int_{\bf R} (\psi(t) - \frac{u}{4\pi^2} \psi''(t)) e(-tu)\ dt. \]

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\).

Lean

Formalized as decay_bounds.

Sources
Leandecay_bounds
Used by 2
Used byDecay bound, alternate form · limiting-fourier-variant

LemmaLimiting Fourier identity#

If \(\psi: \mathbb{R} \to \mathbb{C}\) is \(C^2\) and compactly supported and \(x \geq 1\), 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

By Lemma first-fourier and Lemma second-fourier, we know that for any \(\sigma>1\), we have

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

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

Lean

Formalized as limiting_fourier.

Sources
Leanlimiting_fourier
Uses 2 · Used by 1
Proof usessecond-fourier · first-fourier
Used byCorollary of limiting identity

CorollaryCorollary of limiting identity#

With the hypotheses as above, we have

\[ \sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} ) = A \int_{-\infty}^\infty \hat \psi(\frac{u}{2\pi})\ du + o(1) \]

as \(x \to \infty\).

Proof

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

Lean

Formalized as limiting_cor.

Sources
Leanlimiting_cor
Uses 1 · Used by 1
Proof usesLimiting Fourier identity
Used byLimiting identity for Schwartz functions

LemmaSmooth Urysohn lemma#

If \(I\) is a closed interval contained in an open interval \(J\), then there exists a smooth function \(\Psi: \mathbb{R} \to \mathbb{R}\) with \(1_I \leq \Psi \leq 1_J\).

Proof

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...

Lean

Formalized as smooth_urysohn.

Sources
Leansmooth_urysohn
Used by 1
Used byLimiting identity for Schwartz functions

LemmaLimiting identity for Schwartz functions#

The previous corollary also holds for functions \(\psi\) that are assumed to be in the Schwartz class, as opposed to being \(C^2\) and compactly supported.

Proof

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

\[ |\psi_{>R}(t)|, |\psi''_{>R}(t)| \ll R^{-1} / (1 + |t|^2) \]

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

\[ \hat \psi_{>R}(u) \ll R^{-1} / (1+|u|^2). \]

Using this and (1) one can show that

\[ \sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi_{>R}( \frac{1}{2\pi} \log \frac{n}{x} ), A \int_{-\infty}^\infty \hat \psi_{>R} (\frac{u}{2\pi})\ du \ll R^{-1} \]

(with implied constants also depending on \(A\)), while from Lemma Corollary of limiting identity one has

\[ \sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi_{\leq R}( \frac{1}{2\pi} \log \frac{n}{x} ) = A \int_{-\infty}^\infty \hat \psi_{\leq R} (\frac{u}{2\pi})\ du + o(1). \]

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

Lean

Formalized as limiting_cor_schwartz.

Sources
Leanlimiting_cor_schwartz
Uses 2 · Used by 1
Proof usesCorollary of limiting identity · Smooth Urysohn lemma
Used bySmoothed Wiener-Ikehara

LemmaBijectivity of Fourier transform#

The Fourier transform is a bijection on the Schwartz class. [Note: only surjectivity is actually used.]

Proof

This is a standard result in Fourier analysis. It can be proved here by appealing to Mellin inversion, Theorem MellinInversion. 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.

Lean

Formalized as fourier_surjection_on_schwartz.

Sources
Leanfourier_surjection_on_schwartz
Used by 1
Used bySmoothed Wiener-Ikehara

CorollarySmoothed Wiener-Ikehara#

If \(\Psi: (0,\infty) \to \mathbb{C}\) is smooth and compactly supported away from the origin, then,

\[ \sum_{n=1}^\infty f(n) \Psi( \frac{n}{x} ) = A x \int_0^\infty \Psi(y)\ dy + o(x) \]

as \(x \to \infty\).

Proof

By Lemma Bijectivity of Fourier transform, we can write

\[ y \Psi(y) = \hat \psi( \frac{1}{2\pi} \log y ) \]

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

\[ \sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} ) = A \int_{-\infty}^\infty \hat \psi(\frac{u}{2\pi})\ du + o(1) \]

and the claim follows from Lemma Limiting identity for Schwartz functions.

Lean

Formalized as wiener_ikehara_smooth.

Sources
Leanwiener_ikehara_smooth
Uses 2 · Used by 1
Proof usesLimiting identity for Schwartz functions · Bijectivity of Fourier transform
Used byWiener-Ikehara in an interval

Now we add the hypothesis that \(f(n) \geq 0\) for all \(n\).

PropositionWiener-Ikehara in an interval#

For any closed interval \(I \subset (0,+\infty)\), we have

\[ \sum_{n=1}^\infty f(n) 1_I( \frac{n}{x} ) = A x |I| + o(x). \]
Proof

Use Lemma Smooth Urysohn lemma 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\).

Lean

Formalized as WienerIkeharaInterval.

Sources
LeanWienerIkeharaInterval
Uses 1 · Used by 1
Proof usesSmoothed Wiener-Ikehara
Used byWiener-Ikehara Theorem (1)

CorollaryWiener-Ikehara Theorem (1)#

We have

\[ \sum_{n\leq x} f(n) = A x + o(x). \]
Proof

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

Lean

Formalized as WienerIkeharaTheorem'.

Sources
LeanWienerIkeharaTheorem'
Uses 1 · Used by 4
Proof usesWiener-Ikehara in an interval
Used byauto-cheby · Wiener-Ikehara Theorem (2) · WeakPNT-AP · WeakPNT

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.