From a4d6b1db8f54183d1584340c91021ade2768f8e4 Mon Sep 17 00:00:00 2001 From: AlexKontorovich <58564076+AlexKontorovich@users.noreply.github.com> Date: Tue, 23 Jan 2024 13:40:58 -0500 Subject: [PATCH] Wiener uses --- PrimeNumberTheoremAnd/Wiener.lean | 137 ++++++++++++++++++++++++++ blueprint/ResidueCalcOnRectangles.tex | 11 ++- blueprint/blueprint.tex | 4 +- blueprint/wiener.tex | 30 ++++-- 4 files changed, 173 insertions(+), 9 deletions(-) create mode 100644 PrimeNumberTheoremAnd/Wiener.lean diff --git a/PrimeNumberTheoremAnd/Wiener.lean b/PrimeNumberTheoremAnd/Wiener.lean new file mode 100644 index 00000000..fed5c048 --- /dev/null +++ b/PrimeNumberTheoremAnd/Wiener.lean @@ -0,0 +1,137 @@ +/-%% +The Fourier transform of an absolutely integrable function $\psi: \R \to \C$ is defined by the formula +$$ \hat \psi(u) := \int_\R e(-tu) \psi(t)\ dt$$ +where $e(\theta) := e^{2\pi i \theta}$. + +Let $f: \N \to \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$. + +\begin{lemma}[First Fourier identity]\label{first-fourier} If $\psi: \R \to \C$ is continuous and compactly supported 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_\R F(\sigma + it) \psi(t) x^{it}\ dt.$$ +\end{lemma} + +\begin{proof} By the definition of the Fourier transform, the left-hand side expands as +$$ \sum_{n=1}^\infty \int_\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_\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. +\end{proof} + +\begin{lemma}[Second Fourier identity]\label{second-fourier} If $\psi: \R \to \C$ is continuous and compactly supported 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_\R \frac{1}{\sigma+it-1} \psi(t) x^{it}\ dt.$$ +\end{lemma} + +\begin{proof} +\uses{first-fourier} + The left-hand side expands as + $$ \int_{-\log x}^\infty \int_\R e^{-u(\sigma-1)} \psi(t) e(-\frac{tu}{2\pi})\ dt du = x^{\sigma - 1} \int_\R \frac{1}{\sigma+it-1} \psi(t) x^{it}\ dt$$ + so by Fubini's theorem it suffices to verify the identity +$$ \int_{-\log x}^\infty \int_\R e^{-u(\sigma-1)} e(-\frac{tu}{2\pi})\ du = x^{\sigma - 1} \frac{1}{\sigma+it-1} x^{it}$$ +which is a routine calculation. +\end{proof} + +Now let $A \in \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 +\begin{equation}\label{cheby} +\sum_{n \leq x} |f(n)| \ll x +\end{equation} +for all $x \geq 1$ (this hypothesis is not strictly necessary, but simplifies the arguments and can be obtained fairly easily in applications). + +\begin{lemma}[Decay bounds]\label{decay} If $\psi:\R \to \C$ is $C^2$ and obeys the bounds + $$ |\psi(t)|, |\psi''(t)| \leq A / (1 + |t|^2)$$ + for all $t \in \R$, then +$$ |\hat \psi(u)| \leq C A / (1+|u|^2)$$ +for all $u \in \R$, where $C$ is an absolute constant. +\end{lemma} + +\begin{proof} This follows from a standard integration by parts argument. +\end{proof} + +\begin{lemma}[Limiting Fourier identity]\label{limiting} If $\psi: \R \to \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_\R G(1+it) \psi(t) x^{it}\ dt.$$ +\end{lemma} + +\begin{proof} +\uses{first-fourier,second-fourier,decay} + By the preceding two lemmas, 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_\R G(\sigma+it) \psi(t) x^{it}\ dt.$$ + Now take limits as $\sigma \to 1$ using dominated convergence together with \eqref{cheby} and Lemma \ref{decay} to obtain the result. +\end{proof} + +\begin{corollary}\label{limiting-cor} 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$. +\end{corollary} + +\begin{proof} +\uses{limiting} + Immediate from the Riemann-Lebesgue lemma, and also noting that $\int_{-\infty}^{-\log x} \hat \psi(\frac{u}{2\pi})\ du = o(1)$. +\end{proof} + +\begin{lemma}\label{schwarz-id} 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. +\end{lemma} + +\begin{proof} +\uses{limiting-cor} +For any $R>1$, one can use a smooth cutoff function 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 \ref{decay} we then have +$$ \hat \psi_{>R}(u) \ll R^{-1} / (1+|u|^2).$$ +Using this and \eqref{cheby} 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 \ref{limiting-cor} 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. +\end{proof} + +\begin{lemma}\label{bij} The Fourier transform is a bijection on the Schwartz class. +\end{lemma} + +\begin{proof} This is a standard result in Fourier analysis. +\end{proof} + +\begin{corollary} If $\Psi: (0,\infty) \to \C$ is smooth and compactly supported away from the origin, then, then +$$ \sum_{n=1}^\infty f(n) \Psi( \frac{n}{x} ) = A x \int_0^\infty \Psi(y)\ dy + o(x)$$ +as $u \to \infty$. +\end{corollary} + +\begin{proof} +\uses{bij,schwarz-id} + By Lemma \ref{bij}, 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 \ref{schwarz-id}. +\end{proof} + +\begin{lemma}[Smooth Urysohn lemma]\label{smooth-ury} If $I$ is a closed interval contained in an open interval $J$, then there exists a smooth function $\Psi: \R \to \R$ with $1_I \leq \Psi \leq 1_J$. +\end{lemma} + +\begin{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$. +\end{proof} + +Now we add the hypothesis that $f(n) \geq 0$ for all $n$. + +\begin{proposition} +\label{prop:smooth-ury} + 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).$$ +\end{proposition} + +\begin{proof} +\uses{smooth-ury} + Use Lemma \ref{smooth-ury} 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$. +\end{proof} + +\begin{corollary} We have +$$ \sum_{n\leq x} f(n) = A x |I| + o(x).$$ +\end{corollary} + +\begin{proof} +\uses{prop:smooth-ury} + Apply the preceding proposition with $I = [\varepsilon,1]$ and then send $\varepsilon$ to zero (using \eqref{cheby} to control the error). +\end{proof} + +%%-/ diff --git a/blueprint/ResidueCalcOnRectangles.tex b/blueprint/ResidueCalcOnRectangles.tex index 2497246e..2f4377fd 100644 --- a/blueprint/ResidueCalcOnRectangles.tex +++ b/blueprint/ResidueCalcOnRectangles.tex @@ -21,8 +21,10 @@ -A function is Meromorphic on a rectangle with corners $z$ and $w$ if it is holomorphic off a +\begin{definition}\label{MeromorphicOnRectangle}\lean{MeromorphicOnRectangle}\leanok +A function $f$ is Meromorphic on a rectangle with corners $z$ and $w$ if it is holomorphic off a (finite) set of poles, none of which are on the boundary of the rectangle. +\end{definition} @@ -33,6 +35,13 @@ +\begin{proof} +\uses{MeromorphicOnRectangle, RectangleIntegral} +Rectangles tile rectangles, zoom in. +\end{proof} + + + A meromorphic function has a pole of finite order. \begin{definition}\label{PoleOrder} If $f$ has a pole at $z_0$, then there is an integer $n$ such that diff --git a/blueprint/blueprint.tex b/blueprint/blueprint.tex index 6bbb53a6..4497ed38 100644 --- a/blueprint/blueprint.tex +++ b/blueprint/blueprint.tex @@ -26,6 +26,7 @@ \chapter{The project} +The project github page is \url{https://github.com/AlexKontorovich/PrimeNumberTheoremAnd}. The first main goal is to prove the Prime Number Theorem. Continuations of this project aim to extend this work to primes in progressions (Dirichlet's theorem), Chebytarev's density theorem, etc @@ -41,7 +42,8 @@ \chapter{The project} \chapter{First approach: Wiener-Ikehara Tauberian theorem.} -\input{wiener.tex} +\section{A Fourier-analytic proof of the Wiener-Ikehara theorem} +\input{Wiener.tex} \chapter{Second approach} diff --git a/blueprint/wiener.tex b/blueprint/wiener.tex index 7550679d..7dae6373 100644 --- a/blueprint/wiener.tex +++ b/blueprint/wiener.tex @@ -1,4 +1,3 @@ -\section{A Fourier-analytic proof of the Wiener-Ikehara theorem} The Fourier transform of an absolutely integrable function $\psi: \R \to \C$ is defined by the formula $$ \hat \psi(u) := \int_\R e(-tu) \psi(t)\ dt$$ @@ -25,7 +24,9 @@ \section{A Fourier-analytic proof of the Wiener-Ikehara theorem} $$ \int_{-\log x}^\infty e^{-u(\sigma-1)} \hat \psi(\frac{u}{2\pi})\ du = x^{\sigma - 1} \int_\R \frac{1}{\sigma+it-1} \psi(t) x^{it}\ dt.$$ \end{lemma} -\begin{proof} The left-hand side expands as +\begin{proof} +\uses{first-fourier} + The left-hand side expands as $$ \int_{-\log x}^\infty \int_\R e^{-u(\sigma-1)} \psi(t) e(-\frac{tu}{2\pi})\ dt du = x^{\sigma - 1} \int_\R \frac{1}{\sigma+it-1} \psi(t) x^{it}\ dt$$ so by Fubini's theorem it suffices to verify the identity $$ \int_{-\log x}^\infty \int_\R e^{-u(\sigma-1)} e(-\frac{tu}{2\pi})\ du = x^{\sigma - 1} \frac{1}{\sigma+it-1} x^{it}$$ @@ -52,7 +53,9 @@ \section{A Fourier-analytic proof of the Wiener-Ikehara theorem} $$ \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_\R G(1+it) \psi(t) x^{it}\ dt.$$ \end{lemma} -\begin{proof} By the preceding two lemmas, we know that for any $\sigma>1$, we have +\begin{proof} +\uses{first-fourier,second-fourier,decay} + By the preceding two lemmas, 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_\R G(\sigma+it) \psi(t) x^{it}\ dt.$$ Now take limits as $\sigma \to 1$ using dominated convergence together with \eqref{cheby} and Lemma \ref{decay} to obtain the result. \end{proof} @@ -62,13 +65,16 @@ \section{A Fourier-analytic proof of the Wiener-Ikehara theorem} as $x \to \infty$. \end{corollary} -\begin{proof} Immediate from the Riemann-Lebesgue lemma, and also noting that $\int_{-\infty}^{-\log x} \hat \psi(\frac{u}{2\pi})\ du = o(1)$. +\begin{proof} +\uses{limiting} + Immediate from the Riemann-Lebesgue lemma, and also noting that $\int_{-\infty}^{-\log x} \hat \psi(\frac{u}{2\pi})\ du = o(1)$. \end{proof} \begin{lemma}\label{schwarz-id} 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. \end{lemma} \begin{proof} +\uses{limiting-cor} For any $R>1$, one can use a smooth cutoff function 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 \ref{decay} we then have @@ -91,7 +97,9 @@ \section{A Fourier-analytic proof of the Wiener-Ikehara theorem} as $u \to \infty$. \end{corollary} -\begin{proof} By Lemma \ref{bij}, we can write +\begin{proof} +\uses{bij,schwarz-id} + By Lemma \ref{bij}, 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)$$ @@ -106,11 +114,15 @@ \section{A Fourier-analytic proof of the Wiener-Ikehara theorem} Now we add the hypothesis that $f(n) \geq 0$ for all $n$. -\begin{proposition} For any closed interval $I \subset (0,+\infty)$, we have +\begin{proposition} +\label{prop:smooth-ury} + 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).$$ \end{proposition} -\begin{proof} Use Lemma \ref{smooth-ury} 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$. +\begin{proof} +\uses{smooth-ury} + Use Lemma \ref{smooth-ury} 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$. \end{proof} \begin{corollary} We have @@ -118,5 +130,9 @@ \section{A Fourier-analytic proof of the Wiener-Ikehara theorem} \end{corollary} \begin{proof} +\uses{prop:smooth-ury} Apply the preceding proposition with $I = [\varepsilon,1]$ and then send $\varepsilon$ to zero (using \eqref{cheby} to control the error). \end{proof} + + +