BddAboveOnRect to I5Bound

LemmaBddAboveOnRect#

Let \(g : \mathbb{C} \to \mathbb{C}\) be a holomorphic function on a rectangle, then \(g\) is bounded above on the rectangle.

Proof

Use the compactness of the rectangle and the fact that holomorphic functions are continuous.

Lean

Formalized as BddAboveOnRect.

Sources
LeanBddAboveOnRect

TheoremSmoothedChebyshevPull1#

We have that

\[ \psi_{\epsilon}(X) = \mathcal{M}(\widetilde{1_{\epsilon}})(1) X^{1} + I_1 - I_2 +I_{37} + I_8 + I_9 . \]
Proof

Pull rectangle contours and evaluate the pole at \(s=1\).

Lean

Formalized as SmoothedChebyshevPull1.

Sources
LeanSmoothedChebyshevPull1
Uses 19 · Used by 1
Statement usesI₁ · SmoothedChebyshev · I₃₇ · I₉ · Smooth1 · I₂ · I₈
Proof usesSmooth1Nonneg · ResidueMult · SmoothedChebyshevPull1-aux-integrable · ResidueTheoremOnRectangleWithSimplePole · BddAbove-to-IsBigO · riemannZetaLogDerivResidue · Smooth1Properties-above · existsDifferentiableOn-of-bddAbove · Smooth1ContinuousAt · Smooth1LeOne · RectangleIntegral · VerticalIntegral
Used byGenStrengthPNT

Next pull contours to another box.

LemmaSmoothedChebyshevPull2#

We have that

\[ I_{37} = I_3 - I_4 + I_5 + I_6 + I_7 . \]
Proof

Mimic the proof of Lemma SmoothedChebyshevPull1.

Lean

Formalized as SmoothedChebyshevPull2.

Sources
LeanSmoothedChebyshevPull2
Uses 13 · Used by 1
Statement usesI₃ · I₃₇ · I₄ · Smooth1 · I₆ · I₇ · I₅
Proof usesSmooth1Nonneg · HolomorphicOn.vanishesOnRectangle · Smooth1Properties-above · Smooth1ContinuousAt · Smooth1LeOne · RectangleIntegral
Used byGenStrengthPNT

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

TheoremZetaBoxEval#

For all \(\epsilon > 0\) sufficiently close to \(0\), the rectangle integral over \([1-\delta,2] \times_{ℂ} [-T,T]\) of the integrand in \(\psi_{\epsilon}\) is

\[ \frac{X^{1}}{1}\mathcal{M}(\widetilde{1_{\epsilon}})(1) = X(1+O(\epsilon)) , \]

where the implicit constant is independent of \(X\).

Proof

Unfold the definitions and apply Lemma MellinOfSmooth1c.

Lean

Formalized as ZetaBoxEval.

Sources
LeanZetaBoxEval
Uses 2
Statement usesSmooth1
Proof usesMellinOfSmooth1c

It remains to estimate all of the integrals.

This auxiliary lemma is useful for what follows.

LemmaIBound-aux1#

Given a natural number \(k\) and a real number \(X_0 > 0\), there exists \(C \geq 1\) so that for all \(X \geq X_0\),

\[ \log^k X \le C \cdot X. \]
Proof

We use the fact that \(\log^k X / X\) goes to \(0\) as \(X \to \infty\). Then we use the extreme value theorem to find a constant \(C\) that works for all \(X \geq X_0\).

Lean

Formalized as IBound_aux1.

Sources
LeanIBound_aux1
Used by 1
Used byI2GenBound

LemmaI1Bound#

We have that

\[ \left|I_{1}(\nu, \epsilon, X, T)\ \right| \ll \frac{X\log X}{\epsilon T} . \]
Proof

Unfold the definitions and apply the triangle inequality.

\[ \left|I_{1}(\nu, \epsilon, X, T)\right| = \left| \frac{1}{2\pi i} \int_{-\infty}^{-T} \left( \frac{-\zeta'}\zeta(\sigma_0 + t i) \right) \mathcal M(\widetilde 1_\epsilon)(\sigma_0 + t i) X^{\sigma_0 + t i} \ i \ dt \right| \]

By Theorem dlog-riemannZeta-bdd-on-vertical-lines, \(\zeta'/\zeta (\sigma_0 + t i)\) is bounded by \(\zeta'/\zeta(\sigma_0)\), and Theorem riemannZetaLogDerivResidue gives \(\ll 1/(\sigma_0-1)\) for the latter. This gives:

\[ \leq \frac{1}{2\pi} \left| \int_{-\infty}^{-T} C \log X\cdot \frac{C'}{\epsilon|\sigma_0 + t i|^2} X^{\sigma_0} \ dt \right| , \]

where we used Theorem MellinOfSmooth1b. Continuing the calculation, we have

\[ \leq \log X \cdot C'' \frac{X^{\sigma_0}}{\epsilon} \int_{-\infty}^{-T} \frac{1}{t^2} \ dt \ \leq \ C''' \frac{X\log X}{\epsilon T} , \]

where we used that \(\sigma_0=1+1/\log X\), and \(X^{\sigma_0} = X\cdot X^{1/\log X}=e \cdot X\).

Lean

Formalized as I1Bound.

Sources
LeanI1Bound
Uses 5 · Used by 2
Statement usesI₁
Proof usesSmoothedChebyshevPull1-aux-integrable · riemannZetaLogDerivResidue · Smooth1 · MellinOfSmooth1b
Used byGenStrengthPNT · I9Bound

LemmaI9Bound#

We have that

\[ \left|I_{1}(\nu, \epsilon, X, T)\ \right| \ll \frac{X}{\epsilon T} . \]
Proof

We deduce this from the corresponding bound for \(I_1\), using the symmetry between \(I_1\) and \(I_9\).

Lean

Formalized as I9Bound.

Sources
LeanI9Bound
Uses 5 · Used by 1
Statement usesI₉
Proof usesI₁ · I1Bound · Smooth1 · deriv-riemannZeta-conj
Used byGenStrengthPNT

LemmaI2GenBound#

Assuming a bound of the form of Definition LogDerivZetaHasBound we have that

\[ \left|I_2(\nu,\epsilon,X,T)\right|\ll\frac{X}{\epsilon T}. \]
Proof

Unfold the definitions and apply the triangle inequality.

\[ \left|I_2(\nu, \epsilon, X, T, \sigma_1)\right|= \left|\frac{1}{2\pi i}\int_{\sigma_1}^{\sigma_0} \left(\frac{-\zeta'}\zeta(\sigma - T i) \right) \cdot \mathcal M(\widetilde 1_\epsilon)(\sigma - T i) \cdot X^{\sigma - T i} \ d\sigma \right| \]
\[ \leq \frac{1}{2\pi} \int_{\sigma_1}^{\sigma_0} C \cdot \log T ^{n_2} \frac{C'}{\epsilon|\sigma - T i|^2} X^{\sigma_0} \ d\sigma \leq C'' \cdot \frac{X\log T^{n_2}}{\epsilon T^2} , \]

where we used Theorems MellinOfSmooth1b, the hypothesised bound on zeta and the fact that \(X^\sigma \le X^{\sigma_0} = X\cdot X^{1/\log X}=e \cdot X\). Since \(T>3\), we have \(\log T^{n_2} \leq C''' T\).

Lean

Formalized as I2GenBound.

Sources
LeanI2GenBound
Uses 5 · Used by 2
Statement usesLogDerivZetaHasBound · I₂
Proof usesSmooth1 · IBound-aux1 · MellinOfSmooth1b
Used byGenStrengthPNT · I8GenBound

LemmaI8I2#

Symmetry between \(I_2\) and \(I_8\):

\[ I_8(\nu, \epsilon, X, T) = -\overline{I_2(\nu, \epsilon, X, T)} . \]
Proof

This is a direct consequence of the definitions of \(I_2\) and \(I_8\).

Lean

Formalized as I8I2.

Sources
LeanI8I2
Uses 5 · Used by 1
Statement usesI₂ · I₈
Proof usesSmooth1 · intervalIntegral-conj · deriv-riemannZeta-conj
Used byI8GenBound

LemmaI8GenBound#

Assuming a bound of the form of Definition LogDerivZetaHasBound, we have that

\[ \left|I_8(\nu,\epsilon,X,T)\right|\ll\frac{X}{\epsilon T}. \]
Proof

We deduce this from the corresponding bound for \(I_2\), using the symmetry between \(I_2\) and \(I_8\).

Lean

Formalized as I8GenBound.

Sources
LeanI8GenBound
Uses 5 · Used by 1
Statement usesLogDerivZetaHasBound · I₈
Proof usesI₂ · I2GenBound · I8I2
Used byGenStrengthPNT

LemmaReal.log-le-const-mul-rpow#

For all \(0\lt c\) and \(0\lt x\) we have that

\[ \log x\leq cx^{1/c}. \]
Proof

By Real.log_le_sub_one_of_pos we know that \(\log y\leq y-1\). If we set \(y=x^{1/c}\) this becomes

\[ \frac{\log x}{c}\leq x^{1/c}-1. \]

Multiplying through by \(c\) we have

\[ \log x\leq cx^{1/c}-c\leq cx^{1/c} \]

as desired.

Lean

Formalized as Real.log_le_const_mul_rpow.

Sources
LeanReal.log_le_const_mul_rpow
Used by 1
Used bylog-pow-over-xsq-integral-bounded

Lemmalog-pow-over-xsq-integral-bounded#

For every \(0\lt n\) there exists a constant \(C>0\) (depending on \(n\)) such that

\[ \int_3^T\frac{(\log x)^n}{x^2}dx < C \]
Proof

Using the previous lemma, we know for all \(0\lt c\) and \(0\lt x\) that

\[ (\log x)^n\leq (cx^{1/c})^n=c^nx^{n/c}. \]

Now if we choose \(c=2n\) then

\[ \frac{(\log x)^n}{x^2}\leq (2n)^nx^{-3/2}. \]

This function is dominates the integrand and is integrable in \(x\) by the \(p\)-test.

Lean

Formalized as log_pow_over_xsq_integral_bounded.

Sources
Leanlog_pow_over_xsq_integral_bounded
Uses 1 · Used by 1
Proof usesReal.log-le-const-mul-rpow
Used byI3GenBound

LemmaI3GenBound#

Assuming a bound of the form of Definition LogDerivZetaHasBound, we have that

\[ \left|I_3(\nu,\epsilon,X,T)\right|\ll\frac{X}{\epsilon}\, X^{-\frac{A}{(\log T)^{n_1}}}. \]
Proof

Unfold the definitions and apply the triangle inequality.

\[ \left|I_{3}(\nu, \epsilon, X, T, \sigma_1)\right| = \left|\frac{1}{2\pi i} \int_{-T}^3 \left(\frac{-\zeta'}\zeta(\sigma_1 + t i) \right) \mathcal M(\widetilde 1_\epsilon)(\sigma_1 + t i) X^{\sigma_1 + t i} \ i \ dt \right| \]
\[ \leq \frac{1}{2\pi} \int_{-T}^3 C \cdot\log t^{n_2} \frac{C'}{\epsilon|\sigma_1 + t i|^2} X^{\sigma_1} \ dt , \]

where we used Theorems MellinOfSmooth1b and the hypothesised bound on zeta. Now we estimate \(X^{\sigma_1} = X \cdot X^{-A/ \log T^{n_1}}\), and the integral is absolutely bounded.

Lean

Formalized as I3GenBound.

Sources
LeanI3GenBound
Uses 5 · Used by 2
Statement usesI₃ · LogDerivZetaHasBound
Proof usesSmooth1 · MellinOfSmooth1b · log-pow-over-xsq-integral-bounded
Used byGenStrengthPNT · I7GenBound

LemmaI7GenBound#

Assuming a bound of the form of Definition LogDerivZetaHasBound, we have that

\[ \left|I_7(\nu,\epsilon,X,T)\right|\ll\frac{X}{\epsilon}\, X^{-\frac{A}{(\log T)^{n_1}}}. \]
Proof

We deduce this from the corresponding bound for \(I_3\), using the symmetry between \(I_3\) and \(I_7\).

Lean

Formalized as I7GenBound.

Sources
LeanI7GenBound
Uses 7 · Used by 1
Statement usesLogDerivZetaHasBound · I₇
Proof usesI₃ · I3GenBound · Smooth1 · intervalIntegral-conj · deriv-riemannZeta-conj
Used byGenStrengthPNT

LemmaI4GenBound#

Assuming a bound of the form of Definition LogDerivZetaHasBound, we have that

\[ \left|I_4(\nu,\epsilon,X,\sigma_1,\sigma_2)\right| \ll\frac{X}{\epsilon}\,X^{-\frac{A}{(\log T)^{n_1}}}. \]
Proof

The analysis of \(I_4\) is similar to that of \(I_2\), (in Lemma I2Bound) but even easier. Let \(C\) be the sup of \(-\zeta'/\zeta\) on the curve \(\sigma_2 + 3 i\) to \(1+ 3i\) (this curve is compact, and away from the pole at \(s=1\)). Apply Theorem MellinOfSmooth1b to get the bound \(1/(\epsilon |s|^2)\), which is bounded by \(C'/\epsilon\). And \(X^s\) is bounded by \(X^{\sigma_1}=X \cdot X^{-A/ \log T^{n_1}}\). Putting these together gives the result.

Lean

Formalized as I4GenBound.

Sources
LeanI4GenBound
Uses 3 · Used by 2
Statement usesI₄
Proof usesSmooth1 · MellinOfSmooth1b
Used byGenStrengthPNT · I6GenBound

LemmaI6GenBound#

Assuming a bound of the form of Definition LogDerivZetaHasBound, we have that

\[ \left|I_6(\nu,\epsilon,X,\sigma_1,\sigma_2)\right| \ll\frac{X}{\epsilon}\,X^{-\frac{A}{(\log T)^{n_1}}}. \]
Proof

We deduce this from the corresponding bound for \(I_4\), using the symmetry between \(I_4\) and \(I_6\).

Lean

Formalized as I6GenBound.

Sources
LeanI6GenBound
Uses 6 · Used by 1
Statement usesI₆
Proof usesI₄ · Smooth1 · intervalIntegral-conj · deriv-riemannZeta-conj · I4GenBound
Used byGenStrengthPNT

LemmaI5Bound#

We have that

\[ \left|I_5(\nu,\epsilon,X,\sigma_2)\right|\ll\frac{X^{\sigma_2}}{\epsilon}. \]
Proof

Here \(\zeta'/\zeta\) is absolutely bounded on the compact interval \(\sigma_2 + i [-3,3]\), and \(X^s\) is bounded by \(X^{\sigma_2}\). Using Theorem MellinOfSmooth1b gives the bound \(1/(\epsilon |s|^2)\), which is bounded by \(C'/\epsilon\). Putting these together gives the result.

Lean

Formalized as I5Bound.

Sources
LeanI5Bound
Uses 3 · Used by 1
Statement usesI₅
Proof usesSmooth1 · MellinOfSmooth1b
Used byGenStrengthPNT

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.