SumBoundII to StrongPNT

TheoremSumBoundII #

For all \(t\in\mathbb{R}\) with \(|t|\geq 2\) and \(z=\sigma+it\) where \(1-\delta_t/3\leq\sigma\leq 3/2\), we have that

\[ \left|\frac{\zeta'}{\zeta}(z) -\sum_{\rho\in\mathcal{Z}_t}\frac{m_\zeta(\rho)}{z-\rho}\right|\ll\log|t|. \]

Proof

By Lemma DeltaRange we have that

\[ -29/54<-1/2-\delta_t/3\leq\sigma-3/2\leq0. \]

We apply Theorem LogDerivZetaFinalBound where \(r'=2/3\), \(r=3/4\), \(R'=4/5\), and \(R=5/6\). Thus for all \(z\in\overline{\mathbb{D}_{2/3}}\setminus\mathcal{K}_f(4/5)\) we have that

\[ \left|\frac{\zeta'}{\zeta}(z+3/2+it) -\sum_{\rho\in\mathcal{K}_f(3/4)}\frac{m_f(\rho)}{z-\rho}\right|\ll\log|t| \]

where \(f(z)=\zeta(z+3/2+it)\) for \(t\in\mathbb{R}\) with \(|t|\geq 2\). Now if we let \(z=\sigma-3/2\), then \(z\in(-29/54,0)\subseteq\overline{\mathbb{D}_{2/3}}\). Additionally, \(f(z)=\zeta(\sigma+it)\), where \(\sigma+it\) lies in the zero free region given by Lemma ZeroInequality since \(\sigma\geq 1-\delta_t/3\geq 1-\delta_t\). Thus, \(z\not\in\mathcal{K}_f(4/5)\). So,

\[ \left|\frac{\zeta'}{\zeta}(\sigma+it) -\sum_{\rho\in\mathcal{K}_f(3/4)}\frac{m_f(\rho)}{\sigma-3/2-\rho}\right|\ll\log|t|. \]

But now note that if \(\rho\in\mathcal{K}_f(3/4)\), then \(\zeta(\rho+3/2+it)=0\) and \(|\rho|\leq 3/4\) (and the argument works in reverse). Additionally, note that \(m_f(\rho)=m_\zeta(\rho+3/2+it)\). So changing variables using these facts gives us that

\[ \left|\frac{\zeta'}{\zeta}(\sigma+it) -\sum_{\rho\in\mathcal{Z}_t}\frac{m_\zeta(\rho)}{\sigma+it-\rho}\right|\ll\log|t|. \]

Lean

Formalized as SumBoundII.

Sources

PNT+ blueprint: PrimeNumberTheoremAnd/StrongPNT.lean

LeanSumBoundII

Uses 7 · Used by 1

Statement usesDeltaT · ZeroWindow

Proof usesZeroInequality · ZetaShiftFiniteZeros · SetOfZeros · DeltaRange · LogDerivZetaFinalBound

Used byLogDerivZetaUniformLogSquaredBoundStrip

TheoremGapSize #

Let \(t\in\mathbb{R}\) with \(|t|\geq 3\) and \(z=\sigma+it\) where \(1-\delta_t/3\leq\sigma\leq 3/2\). Additionally, let \(\rho\in\mathcal{Z}_t\). Then we have that

\[ |z-\rho|\geq\delta_t/6. \]

Proof

Let \(\rho=\sigma'+it'\) and note that since \(\rho\in\mathcal{Z}_t\), we have \(t'\in(t-3/4,t+3/4)\). Thus, if \(t>1\) we have

\[ \log|t'|\leq\log|t+3/4|\leq\log|2t|=\log 2+\log|t|\leq 2\log|t|. \]

And otherwise if \(t<-1\) we have

\[ \log|t'|\leq\log|t-3/4|\leq\log|2t|=\log 2+\log|t|\leq 2\log|t|. \]

So by taking reciprocals and multiplying through by a constant we have that \(\delta_t\leq2\delta_{t'}\). Now note that since \(\rho\in\mathcal{Z}_t\) we know that \(\sigma'\leq 1-\delta_{t'}\) by Theorem ZeroInequality (here we use the fact that \(|t|\geq 3\) to give us that \(|t'|\geq 2\)). Thus,

\[ \delta_t/6\leq\delta_{t'}-\delta_t/3 =1-\delta_t/3-(1-\delta_{t'})\leq\sigma-\sigma'\leq|z-\rho|. \]

Lean

Formalized as GapSize.

Sources

PNT+ blueprint: PrimeNumberTheoremAnd/StrongPNT.lean

LeanGapSize

Uses 3 · Used by 1

Statement usesDeltaT · ZeroWindow

Proof usesZeroInequality

Used byLogDerivZetaUniformLogSquaredBoundStrip

TheoremLogDerivZetaUniformLogSquaredBoundStrip #

There exists a constant \(F\in(0,1/42)\) such that for all \(t\in\mathbb{R}\) with \(|t|\geq 3\) one has

\[ 1-\frac{F}{\log|t|}\leq\sigma\leq 3/2 \implies\left|\frac{\zeta'}{\zeta}(\sigma+it)\right|\ll\log^2|t| \]

where the implied constant is uniform in \(\sigma\).

Proof

Take \(F=E/3\) where \(E\) comes from Theorem ZeroInequality. Then we have that \(\sigma\geq 1-\delta_t/3\). So, we apply Lemma SumBoundII, which gives us that

\[ \left|\frac{\zeta'}{\zeta}(z) -\sum_{\rho\in\mathcal{Z}_t}\frac{m_\zeta(\rho)}{z-\rho}\right|\ll\log|t|. \]

Using the reverse triangle inequality and rearranging, we have that

\[ \left|\frac{\zeta'}{\zeta}(z)\right| \leq\sum_{\rho\in\mathcal{Z}_t}\frac{m_\zeta(\rho)}{|z-\rho|}+C\,\log|t| \]

where \(C\) is the implied constant in Lemma SumBoundII. Now applying Lemma GapSize we have that

\[ \left|\frac{\zeta'}{\zeta}(z)\right| \leq\frac{6}{\delta_t}\sum_{\rho\in\mathcal{Z}_t}m_\zeta(\rho)+C\,\log|t|. \]

Now let \(f(z)=\zeta(z+3/2+it)/\zeta(3/2+it)\) with \(\rho=\rho'+3/2+it\). Then if \(\rho\in\mathcal{Z}_t\) we have that

\[ 0=\zeta(\rho)=\zeta(\rho'+3/2+it)=f(\rho') \]

with the same multiplicity of zero, that is \(m_\zeta(\rho)=m_f(\rho')\). And also if \(\rho\in\mathcal{Z}_t\) then

\[ 3/4\geq|\rho-(3/2+it)|=|\rho'|. \]

Thus we change variables to have that

\[ \left|\frac{\zeta'}{\zeta}(z)\right| \leq\frac{6}{\delta_t}\sum_{\rho'\in\mathcal{K}_f(3/4)}m_f(\rho')+C\,\log|t|. \]

Now note that \(f(0)=1\) and for \(|z|\leq 5/6\) we have

\[ |f(z)|=\frac{|\zeta(z+3/2+it)|}{|\zeta(3/2+it)|} \leq\frac{\zeta(3/2)}{\zeta(3)}\cdot(7+2\,|t|)\leq\frac{13\,\zeta(3/2)}{3\,\zeta(3)}\,|t| \]

by Theorems ZetaFixedLowerBound and GlobalBound. Thus by Theorem ZerosBound we have that

\[ \sum_{\rho'\in\mathcal{K}_f(3/4)}m_f(\rho') \leq\frac{\log|t|+\log(13\,\zeta(3/2)/(3\,\zeta(3)))}{\log((5/6)/(3/4))}\leq D\log|t| \]

where \(D\) is taken to be sufficiently large. Recall, by definition that, \(\delta_t=E/\log|t|\) with \(E\) coming from Theorem ZeroInequality. By using this fact and the above, we have that

\[ \left|\frac{\zeta'}{\zeta}(z)\right|\ll\log^2|t|+\log|t| \]

where the implied constant is taken to be bigger than \(6D/E+C\). We know that the RHS is bounded above by \(\ll\log^2|t|\); so the result follows.

Lean

Formalized as LogDerivZetaUniformLogSquaredBoundStrip.

Sources

PNT+ blueprint: PrimeNumberTheoremAnd/StrongPNT.lean

LeanLogDerivZetaUniformLogSquaredBoundStrip

Uses 12 · Used by 2

Statement usesZeroInequality

Proof usesDeltaT · ZetaShiftFiniteZeros · ZerosBound · norm-zeta-strict-mono-ofReal · GlobalBound · SetOfZeros · ZetaFixedLowerBound · SumBoundII · ZeroWindowFinite · ZeroWindow · GapSize

Used byLogDerivZetaUniformLogSquaredBound · StrongPNT

TheoremLogDerivZetaBdd-of-Re-ge-three-halves #

There exists a uniform constant \(C\) such that for \(z=\sigma+it\) one has

\[ 3/2\leq\sigma\implies\left|\frac{\zeta'}{\zeta}(z)\right|\leq C. \]

Proof

Note that

\[ \left|\frac{\zeta'}{\zeta}(z)\right|=\left|\sum_{n=1}^\infty\frac{\Lambda(n)}{n^z}\right|\leq \sum_{n=1}^\infty\frac{\Lambda(n)}{|n^z|}=\sum_{n=1}^\infty\frac{\Lambda(n)}{n^\sigma}\leq \sum_{n=1}^\infty\frac{\Lambda(n)}{n^{3/2}}\lt \infty \]

by vonMangoldtLSeriesSummable.