secondProof uses

PrimeNumberTheoremAnd/MellinCalculus.lean

@@ -22,18 +22,21 @@ might have clunkier calculations, which ``magically'' turn out just right - of c
 /-%%
 It is very convenient to define integrals along vertical lines in the complex plane, as follows.
 \begin{definition}\label{VerticalIntegral}
-Let $f$ be a function from $\mathbb{C}$ to $\mathbb{C}$, and let $σ$ be a real number. Then we define
-$$\int_{(σ)}f(s)ds = \int_{σ-i\infty}^{σ+i\infty}f(s)ds.$$
+Let $f$ be a function from $\mathbb{C}$ to $\mathbb{C}$, and let $\sigma$ be a real number. Then we define
+$$\int_{(\sigma)}f(s)ds = \int_{\sigma-i\infty}^{\sigma+i\infty}f(s)ds.$$
 \end{definition}
+[Note: Better to define $\int_{(\sigma)}$ as $\frac1{2\pi i}\int_{\sigma-i\infty}^{\sigma+i\infty}$??
+There's a factor of $2\pi i$ in such contour integrals...]
 %%-/
 -- definition VerticalIntegral (f : ℂ → ℂ) (σ : ℝ) : ℂ :=
 --   ∫ s : ℝ in {σ} | f s |, f s
 /-%%
 We first prove the following ``Perron-type'' formula.
 \begin{lemma}\label{PerronFormula}
-For $x>0$ and $σ>1$, we have
+For $x>0$ and $\sigma>1$, we have
 $$
-\int_{(σ)}\frac{x^s}{s(s+1)}ds = \begin{cases}
+\frac1{2\pi i}
+\int_{(\sigma)}\frac{x^s}{s(s+1)}ds = \begin{cases}
 1-\frac1x & \text{ if }x>1\\
 0 & \text{ if } x<1
 \end{cases}.
@@ -50,8 +53,8 @@ Pull contours and collect residues. This only involves rectangles, and everythin
 
 /-%%
 \begin{theorem}\label{MellinInversion}
-Let $f$ be a nice function from $\mathbb{R}_{>0}$ to $\mathbb{C}$, and let $σ$ be sufficiently large. Then
-$$f(x) = \frac{1}{2\pi i}\int_{(σ)}\mathcal{M}(f)(s)x^{-s}ds.$$
+Let $f$ be a nice function from $\mathbb{R}_{>0}$ to $\mathbb{C}$, and let $\sigma$ be sufficiently large. Then
+$$f(x) = \frac{1}{2\pi i}\int_{(\sigma)}\mathcal{M}(f)(s)x^{-s}ds.$$
 \end{theorem}
 
 [Note: How ``nice''? Schwartz (on $(0,\infty)$) is certainly enough. As we formalize this, we can add whatever conditions are necessary for the proof to go through.]
@@ -66,10 +69,10 @@ $$
 $$
 Assuming $f$ is Schwartz, say, we now have at least quadratic decay in $s$ of the Mellin transform. Inserting this formula into the inversion formula and Fubini-Tonelli (we now have absolute convergence!) gives:
 $$
-RHS = \frac{1}{2\pi i}\left(\int_{(σ)}\int_0^\infty f''(t)t^{s+1}\frac{1}{s(s+1)}dt\right) x^{-s}ds
+RHS = \frac{1}{2\pi i}\left(\int_{(\sigma)}\int_0^\infty f''(t)t^{s+1}\frac{1}{s(s+1)}dt\right) x^{-s}ds
 $$
 $$
-= \int_0^\infty f''(t) t \left( \frac{1}{2\pi i}\int_{(σ)}(t/x)^s\frac{1}{s(s+1)}ds\right) dt.
+= \int_0^\infty f''(t) t \left( \frac{1}{2\pi i}\int_{(\sigma)}(t/x)^s\frac{1}{s(s+1)}ds\right) dt.
 $$
 Apply the Perron formula to the inside:
 $$

PrimeNumberTheoremAnd/SecondProofPNT.lean

@@ -1,10 +1,8 @@
 
 /-%%
 The approach here is completely standard. We follow the use of $\mathcal{M}(\widetilde{1_{\epsilon}})$ as in Kontorovich 2015.
-
 %%-/
 
-
 /-%%
 It has already been established that zeta doesn't vanish on the 1 line, and has a pole at $s=1$ of order 1.
 We also have that
@@ -31,6 +29,7 @@ $$\psi_{\epsilon}(X) = \sum_{n=1}^\infty \Lambda(n)\widetilde{1_{\epsilon}}(n/X)
 
 /-%%
 \begin{proof}
+\uses{SmoothedChebyshev, MellinInversion}
 We have that
 $$\psi_{\epsilon}(X) = \frac{1}{2\pi i}\int_{(2)}\sum_{n=1}^\infty \frac{\Lambda(n)}{n^s}
 \mathcal{M}(\widetilde{1_{\epsilon}})(s)
@@ -50,37 +49,93 @@ and apply the Mellin inversion formula (Theorem \ref{MellinInversion}).
 The smoothed Chebyshev function is close to the actual Chebyshev function.
 \begin{theorem}\label{SmoothedChebyshevClose}
 We have that
-$$\psi_{\epsilon}(X) = \psi(X) + O(\epsilon X \log X).$$
+$$\psi_{\epsilon}(X) = \psi(X) + O(\epsilon X).$$
 \end{theorem}
 %%-/
 
 /-%%
 \begin{proof}
+\uses{SmoothedChebyshevDirichlet, Smooth1Properties}
 Take the difference. By Lemma \ref{Smooth1Properties}, the sums agree except when $1-c \epsilon \leq n/X \leq 1+c \epsilon$. This is an interval of length $\ll \epsilon X$, and the summands are bounded by $\Lambda(n) \ll \log X$.
+
+This is not enough, as it loses a log! (Which is fine if our target is the strong PNT, with exp-root-log savings, but not here with the ``softer'' approach.) So we will need something like the Selberg sieve (already in Mathlib? Or close?) to conclude that the number of primes in this interval is $\ll \epsilon X / \log X + 1$.
+(The number of prime powers is $\ll X^{1/2}$.)
+And multiplying that by $\Lambda (n) \ll \log X$ gives the desired bound.
 \end{proof}
 %%-/
 
 /-%%
 Returning to the definition of $\psi_{\epsilon}$, fix a large $T$ to be chosen later, and pull contours (via rectangles!) to go
-from $2$ up to $2+iT$, then over to $1+iT$, and up from there to $1+i\infty$ (and symmetrically in the lower half plane). Call
-this path $\gamma$. The
+from $2$ up to $2+iT$, then over to $1+iT$, and up from there to $1+i\infty$ (and symmetrically in the lower half plane).  The
 rectangles involved are all where the integrand is holomorphic, so there is no change.
 \begin{theorem}\label{SmoothedChebyshevPull1}
+\uses{SmoothedChebyshev, RectangleIntegral}
 We have that
-$$\psi_{\epsilon}(X) = \frac{1}{2\pi i}\int_{\gamma}\frac{-\zeta'(s)}{\zeta(s)}
+$$\psi_{\epsilon}(X) = \frac{1}{2\pi i}\int_{\text{curve}}\frac{-\zeta'(s)}{\zeta(s)}
 \mathcal{M}(\widetilde{1_{\epsilon}})(s)
 X^{s}ds.$$
 \end{theorem}
 %%-/
 
 /-%%
 Then, since $\zeta$ doesn't vanish on the 1-line, there is a $\delta$ (depending on $T$), so that the box $[1-\delta,1] \times_{ℂ} [-T,T]$ is free of zeros of $\zeta$.
+\begin{theorem}\label{ZetaNoZerosInBox}
+For any $T>0$, there is a $\delta>0$ so that $[1-\delta,1] \times_{ℂ} [-T,T]$ is free of zeros of $\zeta$.
+\end{theorem}
+%%-/
+
+/-%%
+\begin{proof}
+We have that zeta doesn't vanish on the 1 line and is holomorphic inside the box (except for the pole at $s=1$). If for a height $T>0$, there was no such $\delta$, then there would be a sequence of zeros of $\zeta$ approaching the 1 line, and by compactness, we could find a subsequence of zeros converging to a point on the 1 line. But then $\zeta$ would vanish at that point, a contradiction. (Worse yet, zeta would then be entirely zero...)
+\end{proof}
+%%-/
+
+/-%%
 The rectangle with opposite corners $1-\delta - i T$ and $2+iT$ contains a single pole of $-\zeta'/\zeta$ at $s=1$, and the residue is $1$ (from Theorem \ref{ResidueOfLogDerivative}).
 \begin{theorem}\label{ZeroFreeBox}
 $-\zeta'/\zeta$ is holomorphic on the box $[1-\delta,2] \times_{ℂ} [-T,T]$, except a simple pole with residue $1$ at $s$=1.
 \end{theorem}
 %%-/
 
 /-%%
-Inserting this into $\psi_{\epsilon}$, we get
+\begin{proof}
+\uses{ZetaNoZerosInBox, ResidueOfLogDerivative}
+The proof is as described.
+\end{proof}
+%%-/
+
+/-%%
+We insert this information in $\psi_{\epsilon}$. We add and subtract the integral over the box $[1-\delta,2] \times_{ℂ} [-T,T]$, which we evaluate as follows
+\begin{theorem}\label{ZetaBoxEval}
+The rectangle integral over $[1-\delta,2] \times_{ℂ} [-T,T]$ of the integrand in $\psi_{\epsilon}$ is
+$$\frac{1}{2\pi i}\int_{\partial([1-\delta,2] \times_{ℂ} [-T,T])}\frac{-\zeta'(s)}{\zeta(s)}
+\mathcal{M}(\widetilde{1_{\epsilon}})(s)
+X^{s}ds = \frac{X^{1}}{1}\mathcal{M}(\widetilde{1_{\epsilon}})(1)
+= X\left(\mathcal{M}(\psi)\left(\epsilon\right)\right)
+= X(1+O(\epsilon))
+.$$
+\end{theorem}
+%%-/
+
+/-%%
+\begin{proof}
+\uses{ZeroFreeBox, RectangleIntegral, ResidueOfLogDerivative, MellinOfSmooth1, MellinOfDeltaSpikeAt1}
+Residue calculus / the argument principle.
+\end{proof}
+%%-/
+
+/-%%
+It remains to estimate the contributions from the integrals over the curve $\gamma = \gamma_1 +
+\gamma_2 + \gamma_3 + \gamma_4
++\gamma_5,
+$
+where:
+\begin{itemize}
+\item $\gamma_1$ is the vertical segment from $1-i\infty$ to $1-iT$,
+\item $\gamma_2$ is the horizontal segment from $1-iT$ to $1-\delta-iT$,
+\item $\gamma_3$ is the vertical segment from $1-\delta-iT$ to $1-\delta+iT$,
+\item $\gamma_4$ is the horizontal segment from $1-\delta+iT$ to $1+iT$, and
+\item $\gamma_5$ is the vertical segment from $1+iT$ to $1+i\infty$.
+\end{itemize}
+
 %%-/