ChebyshevPsi to SmoothedChebyshevPull1-aux-integ…

DefinitionChebyshevPsi#

The (second) Chebyshev Psi function is defined as

\[ \psi(x) := \sum_{n \le x} \Lambda(n), \]

where \(\Lambda(n)\) is the von Mangoldt function.

Lean

Formalized as ChebyshevPsi.

Sources
LeanChebyshevPsi
Used by 2
Used byWeakPNT-AP-prelim · StrongPNT

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 the following.

TheoremLogDerivativeDirichlet#

We have that, for \(\Re(s)>1\),

\[ -\frac{\zeta'(s)}{\zeta(s)} = \sum_{n=1}^\infty \frac{\Lambda(n)}{n^s}. \]
Proof

Already in Mathlib.

Lean

Formalized as LogDerivativeDirichlet.

Sources
LeanLogDerivativeDirichlet
Used by 3
Used bySmoothedChebyshevDirichlet · ZeroInequality · LogDerivZetaBdd-of-Re-ge-three-halves

The main object of study is the following inverse Mellin-type transform, which will turn out to be a smoothed Chebyshev function.

DefinitionSmoothedChebyshev#

Fix \(\epsilon>0\), and a bumpfunction supported in \([1/2,2]\). Then we define the smoothed Chebyshev function \(\psi_{\epsilon}\) from \(\mathbb{R}_{>0}\) to \(\mathbb{C}\) by

\[ \psi_{\epsilon}(X) = \frac{1}{2\pi i}\int_{(\sigma)}\frac{-\zeta'(s)}{\zeta(s)} \mathcal{M}(\widetilde{1_{\epsilon}})(s) X^{s}ds, \]

where we'll take \(\sigma = 1 + 1 / \log X\).

Lean

Formalized as SmoothedChebyshev.

Sources
LeanSmoothedChebyshev
Uses 2 · Used by 4
Statement usesSmooth1 · VerticalIntegral
Used byGenStrengthPNT · SmoothedChebyshevClose · SmoothedChebyshevDirichlet · SmoothedChebyshevPull1

LemmaSmoothedChebyshevDirichlet-aux-integrable#

Fix a nonnegative, continuously differentiable function \(F\) on \(\mathbb{R}\) with support in \([1/2,2]\), and total mass one, \(\int_{(0,\infty)} F(x)/x dx = 1\). Then for any \(\epsilon>0\), and \(\sigma\in (1, 2]\), the function

\[ x \mapsto\mathcal{M}(\widetilde{1_{\epsilon}})(\sigma + ix) \]

is integrable on \(\mathbb{R}\).

Proof

By Lemma MellinOfSmooth1b the integrand is \(O(1/t^2)\) as \(t\rightarrow \infty\) and hence the function is integrable.

Lean

Formalized as SmoothedChebyshevDirichlet_aux_integrable.

Sources
LeanSmoothedChebyshevDirichlet_aux_integrable
Uses 6 · Used by 3
Statement usesSmooth1
Proof usesSmooth1Nonneg · Smooth1Properties-above · Smooth1ContinuousAt · Smooth1LeOne · MellinOfSmooth1b
Used bySmoothedChebyshevDirichlet · SmoothedChebyshevDirichlet-aux-tsum-integral · SmoothedChebyshevPull1-aux-integrable

LemmaSmoothedChebyshevDirichlet-aux-tsum-integral#

Fix a nonnegative, continuously differentiable function \(F\) on \(\mathbb{R}\) with support in \([1/2,2]\), and total mass one, \(\int_{(0,\infty)} F(x)/x dx = 1\). Then for any \(\epsilon>0\) and \(\sigma\in(1,2]\), the function \(x \mapsto \sum_{n=1}^\infty \frac{\Lambda(n)}{n^{\sigma+it}} \mathcal{M}(\widetilde{1_{\epsilon}})(\sigma+it) x^{\sigma+it}\) is equal to \(\sum_{n=1}^\infty \int_{(0,\infty)} \frac{\Lambda(n)}{n^{\sigma+it}} \mathcal{M}(\widetilde{1_{\epsilon}})(\sigma+it) x^{\sigma+it}\).

Proof

Interchange of summation and integration.

Lean

Formalized as SmoothedChebyshevDirichlet_aux_tsum_integral.

Sources
LeanSmoothedChebyshevDirichlet_aux_tsum_integral
Uses 6 · Used by 1
Statement usesSmooth1
Proof usesSmooth1Nonneg · Smooth1Properties-above · Smooth1ContinuousAt · SmoothedChebyshevDirichlet-aux-integrable · Smooth1LeOne
Used bySmoothedChebyshevDirichlet

TheoremSmoothedChebyshevDirichlet#

We have that

\[ \psi_{\epsilon}(X) = \sum_{n=1}^\infty \Lambda(n)\widetilde{1_{\epsilon}}(n/X). \]
Proof

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) X^{s}ds. \]

We have enough decay (thanks to quadratic decay of \(\mathcal{M}(\widetilde{1_{\epsilon}})\)) to justify the interchange of summation and integration. We then get

\[ \psi_{\epsilon}(X) = \sum_{n=1}^\infty \Lambda(n)\frac{1}{2\pi i}\int_{(2)} \mathcal{M}(\widetilde{1_{\epsilon}})(s) (n/X)^{-s} ds \]

and apply the Mellin inversion formula.

Lean

Formalized as SmoothedChebyshevDirichlet.

Sources
LeanSmoothedChebyshevDirichlet
Uses 9 · Used by 1
Statement usesSmoothedChebyshev · Smooth1
Proof usesSmooth1Nonneg · Smooth1Properties-above · Smooth1ContinuousAt · SmoothedChebyshevDirichlet-aux-integrable · LogDerivativeDirichlet · Smooth1LeOne · SmoothedChebyshevDirichlet-aux-tsum-integral
Used bySmoothedChebyshevClose

The smoothed Chebyshev function is close to the actual Chebyshev function.

TheoremSmoothedChebyshevClose#

We have that

\[ \psi_{\epsilon}(X) = \psi(X) + O(\epsilon X \log X). \]
Proof

Take the difference. By Lemma Smooth1Properties-above and Smooth1Properties-below, 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\).

Lean

Formalized as SmoothedChebyshevClose.

Sources
LeanSmoothedChebyshevClose
Uses 7 · Used by 1
Statement usesSmoothedChebyshev
Proof usesSmooth1Nonneg · SmoothedChebyshevDirichlet · Smooth1Properties-above · Smooth1Properties-below · Smooth1 · Smooth1LeOne
Used byGenStrengthPNT

DefinitionLogDerivZetaHasBound#

For constants \(A\), \(C\), \(n_1\), and \(n_2\) this is true if for all \(3<|t|\) one has

\[ 1-\frac{A}{\log|t|^{n_1}}\leq\sigma\implies|(\zeta'/\zeta)(\sigma+it)|\leq C\,\log|t|^{n_2}. \]
Lean

Formalized as LogDerivZetaHasBound.

Sources
LeanLogDerivZetaHasBound
Used by 7
Used byGenStrengthPNT · MediumPNT · I2GenBound · I3GenBound · I7GenBound · I8GenBound · StrongPNT

Suppose we have an estimate of the form in Definition LogDerivZetaHasBound. Returning to the definition of \(\psi_{\epsilon}\), fix a large \(T\) to be chosen later, and set \(\sigma_0 = 1 + 1 / log X\), \(\sigma_1 = 1- A/ \log T^{n_1}\) (where \(n_1\) comes from our estimate from Definition LogDerivZetaHasBound), and \(\sigma_2\lt \sigma_1\) a constant. Pull contours (via rectangles!) to go from \(\sigma_0-i\infty\) up to \(\sigma_0-iT\), then over to \(\sigma_1-iT\), up to \(\sigma_1-3i\), over to \(\sigma_2-3i\), up to \(\sigma_2+3i\), back over to \(\sigma_1+3i\), up to \(\sigma_1+iT\), over to \(\sigma_0+iT\), and finally up to \(\sigma_0+i\infty\).

In the process, we will pick up the residue at \(s=1\). We will do this in several stages. Here the interval integrals are defined as follows:

DefinitionI₁#

\[ I_1(\nu, \epsilon, X, T) := \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 \]
Lean

Formalized as I₁.

Sources
LeanI₁
Uses 1 · Used by 4
Statement usesSmooth1
Used byGenStrengthPNT · I1Bound · I9Bound · SmoothedChebyshevPull1

DefinitionI₂#

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

Formalized as I₂.

Sources
LeanI₂
Uses 1 · Used by 5
Statement usesSmooth1
Used byGenStrengthPNT · I2GenBound · I8GenBound · I8I2 · SmoothedChebyshevPull1

DefinitionI₃₇#

\[ I_{37}(\nu, \epsilon, X, T, \sigma_1) := \frac{1}{2\pi i} \int_{-T}^{T} \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 \]
Lean

Formalized as I₃₇.

Sources
LeanI₃₇
Uses 1 · Used by 3
Statement usesSmooth1
Used byGenStrengthPNT · SmoothedChebyshevPull1 · SmoothedChebyshevPull2

DefinitionI₈#

\[ I_8(\nu, \epsilon, X, T, \sigma_1) := \frac{1}{2\pi i} \int_{\sigma_1}^{\sigma_0} \left( \frac{-\zeta'}\zeta(\sigma + T i) \right) \mathcal M(\widetilde 1_\epsilon)(\sigma + T i) X^{\sigma + T i} \ d\sigma \]
Lean

Formalized as I₈.

Sources
LeanI₈
Uses 1 · Used by 4
Statement usesSmooth1
Used byGenStrengthPNT · I8GenBound · I8I2 · SmoothedChebyshevPull1

DefinitionI₉#

\[ I_9(\nu, \epsilon, X, T) := \frac{1}{2\pi i} \int_{T}^{\infty} \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 \]
Lean

Formalized as I₉.

Sources
LeanI₉
Uses 1 · Used by 3
Statement usesSmooth1
Used byGenStrengthPNT · I9Bound · SmoothedChebyshevPull1

DefinitionI₃#

\[ I_3(\nu, \epsilon, X, T, \sigma_1) := \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 \]
Lean

Formalized as I₃.

Sources
LeanI₃
Uses 1 · Used by 4
Statement usesSmooth1
Used byGenStrengthPNT · I3GenBound · I7GenBound · SmoothedChebyshevPull2

DefinitionI₇#

\[ I_7(\nu, \epsilon, X, T, \sigma_1) := \frac{1}{2\pi i} \int_{3}^{T} \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 \]
Lean

Formalized as I₇.

Sources
LeanI₇
Uses 1 · Used by 3
Statement usesSmooth1
Used byGenStrengthPNT · I7GenBound · SmoothedChebyshevPull2

DefinitionI₄#

\[ I_4(\nu, \epsilon, X, \sigma_1, \sigma_2) := \frac{1}{2\pi i} \int_{\sigma_2}^{\sigma_1} \left( \frac{-\zeta'}\zeta(\sigma - 3 i) \right) \mathcal M(\widetilde 1_\epsilon)(\sigma - 3 i) X^{\sigma - 3 i} \ d\sigma \]
Lean

Formalized as I₄.

Sources
LeanI₄
Uses 1 · Used by 4
Statement usesSmooth1
Used byGenStrengthPNT · I4GenBound · I6GenBound · SmoothedChebyshevPull2

DefinitionI₆#

\[ I_6(\nu, \epsilon, X, \sigma_1, \sigma_2) := \frac{1}{2\pi i} \int_{\sigma_2}^{\sigma_1} \left( \frac{-\zeta'}\zeta(\sigma + 3 i) \right) \mathcal M(\widetilde 1_\epsilon)(\sigma + 3 i) X^{\sigma + 3 i} \ d\sigma \]
Lean

Formalized as I₆.

Sources
LeanI₆
Uses 1 · Used by 3
Statement usesSmooth1
Used byGenStrengthPNT · I6GenBound · SmoothedChebyshevPull2

DefinitionI₅#

\[ I_5(\nu, \epsilon, X, \sigma_2) := \frac{1}{2\pi i} \int_{-3}^{3} \left( \frac{-\zeta'}\zeta(\sigma_2 + t i) \right) \mathcal M(\widetilde 1_\epsilon)(\sigma_2 + t i) X^{\sigma_2 + t i} \ i \ dt \]
Lean

Formalized as I₅.

Sources
LeanI₅
Uses 1 · Used by 3
Statement usesSmooth1
Used byGenStrengthPNT · I5Bound · SmoothedChebyshevPull2

Lemmadlog-riemannZeta-bdd-on-vertical-lines#

For \(\sigma_0 > 1\), there exists a constant \(C > 0\) such that

\[ \forall t \in \mathbb{R}, \quad \left\| \frac{\zeta'(\sigma_0 + t i)}{\zeta(\sigma_0 + t i)} \right\| \leq C. \]
Proof

Write as Dirichlet series and estimate trivially using Theorem LogDerivativeDirichlet.

Lean

Formalized as dlog_riemannZeta_bdd_on_vertical_lines.

Sources
Leandlog_riemannZeta_bdd_on_vertical_lines
Used by 1
Used bySmoothedChebyshevPull1-aux-integrable

LemmaSmoothedChebyshevPull1-aux-integrable#

The integrand

\[ \zeta'(s)/\zeta(s)\mathcal{M}(\widetilde{1_{\epsilon}})(s)X^{s} \]

is integrable on the contour \(\sigma_0 + t i\) for \(t \in \mathbb{R}\) and \(\sigma_0 > 1\).

Proof

The \(\zeta'(s)/\zeta(s)\) term is bounded, as is \(X^s\), and the smoothing function \(\mathcal{M}(\widetilde{1_{\epsilon}})(s)\) decays like \(1/|s|^2\) by Theorem MellinOfSmooth1b. Actually, we already know that \(\mathcal{M}(\widetilde{1_{\epsilon}})(s)\) is integrable from Theorem SmoothedChebyshevDirichlet-aux-integrable, so we should just need to bound the rest.

Lean

Formalized as SmoothedChebyshevPull1_aux_integrable.

Sources
LeanSmoothedChebyshevPull1_aux_integrable
Uses 3 · Used by 2
Statement usesSmooth1
Proof usesdlog-riemannZeta-bdd-on-vertical-lines · SmoothedChebyshevDirichlet-aux-integrable
Used byI1Bound · SmoothedChebyshevPull1

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.