Zeta0EqZeta to LogDerivZetaHolcLargeT9

LemmaZeta0EqZeta#

For \(\Re(s)>0\), \(s\ne1\), and for any \(N\),

\[ \zeta_0(N,s) = \zeta(s). \]
Proof

Use Lemma ZetaSum-aux2 and the Definition riemannZeta0.

Lean

Formalized as Zeta0EqZeta.

Sources
LeanZeta0EqZeta
Uses 4 · Used by 3
Statement usesriemannZeta0
Proof usesisPathConnected-aux · ZetaSum-aux2 · HolomorphicOn-riemannZeta0
Used byZetaDerivUpperBnd · ZetaUpperBnd · ZetaAltFormula

LemmaZetaBnd-aux2#

Given \(n ≤ t\) and \(\sigma\) with \(1-A/\log t \le \sigma\), we have that

\[ |n^{-s}| \le n^{-1} e^A. \]
Proof

Use \(|n^{-s}| = n^{-\sigma} = e^{-\sigma \log n} \le \exp(-\left(1-\frac{A}{\log t}\right)\log n) \le n^{-1} e^A\), since \(n\le t\).

Lean

Formalized as ZetaBnd_aux2.

Sources
LeanZetaBnd_aux2
Used by 2
Used byZetaDerivUpperBnd · ZetaUpperBnd

LemmaZetaUpperBnd#

For any \(s = \sigma + tI \in \mathbb{C}\), \(1/2 \le \sigma\le 2, 3 < |t|\) and any \(0 < A < 1\) sufficiently small, and \(1-A/\log |t| \le \sigma\), we have

\[ |\zeta(s)| \ll \log t. \]
Proof

First replace \(\zeta(s)\) by \(\zeta_0(N,s)\) for \(N = \lfloor |t| \rfloor\). We estimate:

\[ |\zeta_0(N,s)| \ll \sum_{1\le n \le |t|} |n^{-s}| + \frac{- |t|^{1-\sigma}}{|1-s|} + \frac{-|t|^{-\sigma}}{2} + |t| \cdot |t| ^ {-σ} / σ \]
\[ \ll e^A \sum_{1\le n < |t|} n^{-1} +|t|^{1-\sigma}, \]

where we used Lemma ZetaBnd-aux2 and Lemma ZetaBnd-aux1. The first term is \(\ll \log |t|\). For the second term, estimate

\[ |t|^{1-\sigma} \le |t|^{1-(1-A/\log |t|)} = |t|^{A/\log |t|} \ll 1. \]
Lean

Formalized as ZetaUpperBnd.

Sources
LeanZetaUpperBnd
Uses 4 · Used by 3
Proof usesZetaBnd-aux2 · riemannZeta0 · ZetaBnd-aux1 · Zeta0EqZeta
Used byZetaDerivUpperBnd · ZetaInvBound2 · ZetaLowerBound3

LemmaDerivUpperBnd-aux7#

For any \(s = \sigma + tI \in \mathbb{C}\), \(1/2 \le \sigma\le 2, 3 < |t|\), and any \(0 < A < 1\) sufficiently small, and \(1-A/\log |t| \le \sigma\), we have

\[ \left\|s \cdot \int_{N}^{\infty} \left(\left\lfloor x \right\rfloor + \frac{1}{2} - x\right) \cdot x^{-s-1} \cdot (-\log x) \right\| \le 2 \cdot |t| \cdot N^{-\sigma} / \sigma \cdot \log |t|. \]
Proof

Estimate \(|s|= |\sigma + tI|\) by \(|s|\le 2 +|t| \le 2|t|\) (since \(|t|>3\)). Estimating \(|\left\lfloor x \right\rfloor+1/2-x|\) by \(1\), and using \(|x^{-s-1}| = x^{-\sigma-1}\), we have

\[ \left\| s \cdot \int_{N}^{\infty} \left(\left\lfloor x \right\rfloor + \frac{1}{2} - x\right) \cdot x^{-s-1} \cdot (-\log x) \right\| \le 2 \cdot |t| \int_{N}^{\infty} x^{-\sigma} \cdot (\log x). \]

For the last integral, integrate by parts, getting:

\[ \int_{N}^{\infty} x^{-\sigma-1} \cdot (\log x) = \frac{1}{\sigma}N^{-\sigma} \cdot \log N + \frac1{\sigma^2} \cdot N^{-\sigma}. \]

Now use \(\log N \le \log |t|\) to get the result.

Lean

Formalized as DerivUpperBnd_aux7.

Sources
LeanDerivUpperBnd_aux7
Used by 1
Used byZetaDerivUpperBnd

LemmaZetaDerivUpperBnd#

For any \(s = \sigma + tI \in \mathbb{C}\), \(1/2 \le \sigma\le 2, 3 < |t|\), there is an \(A>0\) so that for \(1-A/\log t \le \sigma\), we have

\[ |\zeta'(s)| \ll \log^2 t. \]
Proof

First replace \(\zeta(s)\) by \(\zeta_0(N,s)\) for \(N = \lfloor |t| \rfloor\). Differentiating term by term, we get:

\[ \zeta'(s) = -\sum_{1\le n < N} n^{-s} \log n + \frac{N^{1 - s}}{(1 - s)^2} + \frac{N^{1 - s} \log N} {1 - s} + \frac{N^{-s}\log N}{2} + \int_N^\infty \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx -s \int_N^\infty \log x \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx . \]

Estimate as before, with an extra factor of \(\log |t|\).

Lean

Formalized as ZetaDerivUpperBnd.

Sources
LeanZetaDerivUpperBnd
Uses 6 · Used by 2
Proof usesZetaBnd-aux2 · ZetaUpperBnd · DerivUpperBnd-aux7 · riemannZeta0 · ZetaBnd-aux1 · Zeta0EqZeta
Used byLogDerivZetaBnd · Zeta-diff-Bnd

LemmaZetaNear1BndFilter#

As \(\sigma\to1^+\),

\[ |\zeta(\sigma)| \ll 1/(\sigma-1). \]
Proof

Zeta has a simple pole at \(s=1\). Equivalently, \(\zeta(s)(s-1)\) remains bounded near \(1\). Lots of ways to prove this. Probably the easiest one: use the expression for \(\zeta_0 (N,s)\) with \(N=1\) (the term \(N^{1-s}/(1-s)\) being the only unbounded one).

Lean

Formalized as ZetaNear1BndFilter.

Sources
LeanZetaNear1BndFilter
Used by 1
Used byZetaNear1BndExact

LemmaZetaNear1BndExact#

There exists a \(c>0\) such that for all \(1 < \sigma ≤ 2\),

\[ |\zeta(\sigma)| ≤ c/(\sigma-1). \]
Proof

Split into two cases, use Lemma ZetaNear1BndFilter for \(\sigma\) sufficiently small and continuity on a compact interval otherwise.

Lean

Formalized as ZetaNear1BndExact.

Sources
LeanZetaNear1BndExact
Uses 1 · Used by 2
Proof usesZetaNear1BndFilter
Used byZetaInvBound2 · ZetaLowerBound3

LemmaZetaLowerBound3#

There exists a \(c>0\) such that for all \(1 < \sigma <= 2\) and \(3 < |t|\),

\[ c \frac{(\sigma-1)^{3/4}}{(\log |t|)^{1/4}} \le |\zeta(\sigma + tI)|. \]
Proof

Combine Lemma ZetaLowerBound2 with upper bounds for \(|\zeta(\sigma)|\) (from Lemma ZetaNear1BndExact) and \(|\zeta(\sigma+2it)|\) (from Lemma ZetaUpperBnd).

Lean

Formalized as ZetaLowerBound3.

Sources
LeanZetaLowerBound3
Uses 2 · Used by 1
Proof usesZetaUpperBnd · ZetaNear1BndExact
Used byZetaLowerBnd

LemmaZetaInvBound1#

For all \(\sigma>1\),

\[ 1/|\zeta(\sigma+it)| \le |\zeta(\sigma)|^{3/4}|\zeta(\sigma+2it)|^{1/4} \]
Proof

The identity

\[ 1 \le |\zeta(\sigma)|^3 |\zeta(\sigma+it)|^4 |\zeta(\sigma+2it)| \]

for \(\sigma>1\) is already proved by Michael Stoll in the EulerProducts PNT file.

Lean

Formalized as ZetaInvBound1.

Sources
LeanZetaInvBound1
Used by 1
Used byZetaInvBound2

LemmaZetaInvBound2#

For \(\sigma>1\) (and \(\sigma \le 2\)),

\[ 1/|\zeta(\sigma+it)| \ll (\sigma-1)^{-3/4}(\log |t|)^{1/4}, \]

as \(|t|\to\infty\).

Proof

Combine Lemma ZetaInvBound1 with the bounds in Lemmata ZetaNear1BndExact and ZetaUpperBnd.

Lean

Formalized as ZetaInvBound2.

Sources
LeanZetaInvBound2
Uses 3 · Used by 1
Proof usesZetaUpperBnd · ZetaInvBound1 · ZetaNear1BndExact
Used byZetaInvBnd

LemmaZeta-eq-int-derivZeta#

For any \(t\ne0\) (so we don't pass through the pole), and \(\sigma_1 < \sigma_2\),

\[ \int_{\sigma_1}^{\sigma_2}\zeta'(\sigma + it) dt = \zeta(\sigma_2+it) - \zeta(\sigma_1+it). \]
Proof

This is the fundamental theorem of calculus.

Lean

Formalized as Zeta_eq_int_derivZeta.

Sources
LeanZeta_eq_int_derivZeta
Used by 1
Used byZeta-diff-Bnd

LemmaZeta-diff-Bnd#

For any \(A>0\) sufficiently small, there is a constant \(C>0\) so that whenever \(1- A / \log t \le \sigma_1 < \sigma_2\le 2\) and \(3 < |t|\), we have that:

\[ |\zeta (\sigma_2 + it) - \zeta (\sigma_1 + it)| \le C (\log |t|)^2 (\sigma_2 - \sigma_1). \]
Proof

Use Lemma Zeta-eq-int-derivZeta and estimate trivially using Lemma ZetaDerivUpperBnd.

Lean

Formalized as Zeta_diff_Bnd.

Sources
LeanZeta_diff_Bnd
Uses 2 · Used by 2
Proof usesZeta-eq-int-derivZeta · ZetaDerivUpperBnd
Used byZetaInvBnd · ZetaLowerBnd

LemmaZetaInvBnd#

For any \(A>0\) sufficiently small, there is a constant \(C>0\) so that whenever \(1- A / \log^9 |t| \le \sigma < 1+A/\log^9 |t|\) and \(3 < |t|\), we have that:

\[ 1/|\zeta(\sigma+it)| \le C \log^7 |t|. \]
Proof

Let \(\sigma\) be given in the prescribed range, and set \(\sigma' := 1+ A / \log^9 |t|\). Then

\[ |\zeta(\sigma+it)| \ge |\zeta(\sigma'+it)| - |\zeta(\sigma+it) - \zeta(\sigma'+it)| \ge C (\sigma'-1)^{3/4}\log |t|^{-1/4} - C \log^2 |t| (\sigma'-\sigma) \]
\[ \ge C A^{3/4} \log |t|^{-7} - C \log^2 |t| (2 A / \log^9 |t|), \]

where we used Lemma ZetaInvBound2 and Lemma Zeta-diff-Bnd. Now by making \(A\) sufficiently small (in particular, something like \(A = 1/16\) should work), we can guarantee that

\[ |\zeta(\sigma+it)| \ge \frac C 2 (\log |t|)^{-7}, \]

as desired.

Lean

Formalized as ZetaInvBnd.

Sources
LeanZetaInvBnd
Uses 2 · Used by 1
Proof usesZetaInvBound2 · Zeta-diff-Bnd
Used byLogDerivZetaBnd

Annoyingly, it is not immediate from this that \(\zeta\) doesn't vanish there! That's because \(1/0 = 0\) in Lean. So we give a second proof of the same fact (refactor this later), with a lower bound on \(\zeta\) instead of upper bound on \(1 / \zeta\).

LemmaZetaLowerBnd#

For any \(A>0\) sufficiently small, there is a constant \(C>0\) so that whenever \(1- A / \log^9 |t| \le \sigma < 1\) and \(3 < |t|\), we have that:

\[ |\zeta(\sigma+it)| \ge C \log^7 |t|. \]
Proof

Follow same argument.

Lean

Formalized as ZetaLowerBnd.

Sources
LeanZetaLowerBnd
Uses 2 · Used by 1
Proof usesZetaLowerBound3 · Zeta-diff-Bnd
Used byZetaZeroFree9

Now we get a zero free region.

LemmaZetaZeroFree9#

There is an \(A>0\) so that for \(1-A/\log^9 |t| \le \sigma < 1\) and \(3 < |t|\),

\[ \zeta(\sigma+it) \ne 0. \]
Proof

Apply Lemma ZetaLowerBnd.

Lean

Formalized as ZetaZeroFree9.

Sources
LeanZetaZeroFree9
Uses 1 · Used by 1
Proof usesZetaLowerBnd
Used byLogDerivZetaHolcLargeT9

LemmaLogDerivZetaBnd#

There is an \(A>0\) so that for \(1-A/\log^9 |t| \le \sigma < 1+A/\log^9 |t|\) and \(3 < |t|\),

\[ |\frac {\zeta'}{\zeta} (\sigma+it)| \ll \log^9 |t|. \]
Proof

Combine the bound on \(|\zeta'|\) from Lemma ZetaDerivUpperBnd with the bound on \(1/|\zeta|\) from Lemma ZetaInvBnd.

Lean

Formalized as LogDerivZetaBnd.

Sources
LeanLogDerivZetaBnd
Uses 2 · Used by 1
Proof usesZetaDerivUpperBnd · ZetaInvBnd
Used byLogDerivZetaBndUnif99

TheoremZetaNoZerosOn1Line#

The zeta function does not vanish on the 1-line.

Proof

This fact is already proved in Stoll's work.

Lean

Formalized as ZetaNoZerosOn1Line.

Sources
LeanZetaNoZerosOn1Line

Then, since \(\zeta\) doesn't vanish on the 1-line, there is a \(\sigma<1\) (depending on \(T\)), so that the box \([\sigma,1] \times_{ℂ} [-T,T]\) is free of zeros of \(\zeta\).

LemmaZetaNoZerosInBox#

For any \(T>0\), there is a constant \(\sigma<1\) so that

\[ \zeta(\sigma'+it) \ne 0 \]

for all \(|t| \leq T\) and \(\sigma' \ge \sigma\).

Proof

Assume not. Then there is a sequence \(|t_n| \le T\) and \(\sigma_n \to 1\) so that \(\zeta(\sigma_n + it_n) = 0\). By compactness, there is a subsequence \(t_{n_k} \to t_0\) along which \(\zeta(\sigma_{n_k} + it_{n_k}) = 0\). If \(t_0\ne0\), use the continuity of \(\zeta\) to get that \(\zeta(1 + it_0) = 0\); this is a contradiction. If \(t_0=0\), \(\zeta\) blows up near \(1\), so can't be zero nearby.

Lean

Formalized as ZetaNoZerosInBox.

Sources
LeanZetaNoZerosInBox
Used by 3
Used byLogDerivZetaHolcLargeT9 · LogDerivZetaHolcSmallT · StrongPNT

We now prove that there's an absolute constant \(\sigma_0\) so that \(\zeta'/\zeta\) is holomorphic on a rectangle \([\sigma_2,2] \times_{ℂ} [-3,3] \setminus \{1\}\).

LemmaLogDerivZetaHolcSmallT#

There is a \(\sigma_2 < 1\) so that the function

\[ \frac {\zeta'}{\zeta}(s) \]

is holomorphic on \(\{ \sigma_2 \le \Re s \le 2, |\Im s| \le 3 \} \setminus \{1\}\).

Proof

The derivative of \(\zeta\) is holomorphic away from \(s=1\); the denominator \(\zeta(s)\) is nonzero in this range by Lemma ZetaNoZerosInBox.

Lean

Formalized as LogDerivZetaHolcSmallT.

Sources
LeanLogDerivZetaHolcSmallT
Uses 1 · Used by 1
Proof usesZetaNoZerosInBox
Used byGenStrengthPNT

LemmaLogDerivZetaHolcLargeT9#

There is an \(A>0\) so that for all \(T>3\), the function \(\frac {\zeta'}{\zeta}(s)\) is holomorphic on \(\{1-A/\log^9 T \le \Re s \le 2, |\Im s|\le T \}\setminus\{1\}\).

Proof

The derivative of \(\zeta\) is holomorphic away from \(s=1\); the denominator \(\zeta(s)\) is nonzero in this range by Lemma ZetaZeroFree9.

Lean

Formalized as LogDerivZetaHolcLargeT9.

Sources
LeanLogDerivZetaHolcLargeT9
Uses 2 · Used by 1
Proof usesZetaZeroFree9 · ZetaNoZerosInBox
Used byMediumPNT

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.