Wiener uses

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}
+
+%%-/

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

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}
 

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,17 +114,25 @@ \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
 $$ \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}
+
+
+