4 Zero Free Region

Definition 484 Log derivative

✓

For \(s\in {\mathbb C}\) define \(Z(s) = \frac{\zeta '(s)}{\zeta (s)}\).

Definition 485 Zero set

✓

Define the set \(\mathcal{Z} = \{ \sigma +it\in {\mathbb C}: \sigma ,t\in {\mathbb R}\; {\rm and}\; \zeta (\sigma +it)=0 \} \).

Definition 486 Window zeros

✓

For \(t\in {\mathbb R}\) define the set

\[ \mathcal{Z}_t = \{ \rho _1=\sigma _1+it_1\in {\mathbb C}: \zeta (\rho _1)=0 \; {\rm and} \; |\rho _1 - (3/2+it)| \le 5/6\} \]

Lemma 487 Finite set

✓

For each \(t\in {\mathbb R}\) the set \(\mathcal Z_t\) is finite.

Proof ▶

Lemma 488 Reciprocal real

✓

Let \(z\in {\mathbb C}\). If \(\Re (z){\gt}0\) then \(\Re (1/z){\gt}0\).

Proof ▶

Lemma 489 Zero free

✓

Let \(\sigma ,t\in {\mathbb R}\). If \(\sigma {\gt} 1\) then \(\zeta (\sigma + it) \neq 0 \).

Proof ▶

Use lemma _root_.riemannZeta_ne_zero_of_one_le_re

in Nonvanishing.lean in Mathlib / NumberTheory / LSeries .

Lemma 490 Zero bound

✓

Let \(\sigma _1,t_1\in {\mathbb R}\). If \(\zeta (\sigma _1 + it_1) = 0\) then \(\sigma _1\le 1\).

Proof ▶

Contrapositive of Lemma 489.

Lemma 491 Zero bound

✓

Let \(t\in {\mathbb R}\). If \(\rho _1=\sigma _1+it_1\in \mathcal Z_t\) then \(\sigma _1\le 1\).

Proof ▶

By definition 486 \(\rho _1\in \mathcal Z_t\) implies \(\zeta (\rho _1)=0\). Now apply Lemma 490.

Lemma 492 Outside zeros

✓

For \(\delta {\gt}0\) and \(t\in {\mathbb R}\), let \(s=1+\delta +it\). Then \(s\notin \mathcal Z_t\).

Proof ▶

We have \(\Re (s)=1+\delta {\gt}1\) since \(\delta {\gt}0\). Thus \(\zeta (s)\neq 0\) by lemma 468, and so \(s\notin \mathcal Z_t\).

Lemma 493 Half disk

✓

For \(0{\lt}\delta {\lt}1\) and \(t\in {\mathbb R}\), let \(c=3/2+it\). Then \(1+\delta +it\in \mathcal{\mathbb D}_{1/2}(c)\).

Proof ▶

We calculate \(1+\delta +it - c = 1+\delta - 3/2 = 1/2-\delta \). Hence \(|(1+\delta +it) - c| \le |1/2-\delta | \le 1/2\) so \(1+\delta +it\in \mathcal{\mathbb D}_{1/2}(c)\).

Lemma 494 Sum bound

✓

There exists a constant \(C{\gt}0\) such that for all \(0{\lt}\delta {\lt}1\) and \(t\in {\mathbb R}\), we have

\[ \left| \sum _{\rho _1\in \mathcal Z_t} \frac{m_{\rho _1,\zeta }}{1+\delta +it-\rho _1} - Z(1+\delta +it)\right| \le C\log (|t|+2). \]

Proof ▶

Apply Lemma 483 with \(z=1+\delta +it\) and \(r_1=1/2\) and \(r=2/3\). For \(c = 3/2+it\), note \(z\in {\mathbb D}_{r_1}(c)\) by lemma 493. Further \(\mathcal Z_t = \mathcal K_\zeta (5/6;c)\) and \(z\notin \mathcal K_\zeta (5/6;c)\) by lemma 492. We choose \(C_1=C(\frac{1}{(r-r_1)^3}+1)\).

Lemma 495 Real bound

✓

There exists a constant \(C{\gt}0\) such that for all \(0{\lt}\delta {\lt}1\) and \(t\in {\mathbb R}\), we have

\[ \Re \left(\sum _{\rho _1\in \mathcal Z_t} \frac{m_{\rho _1,\zeta }}{1+\delta +it-\rho _1} - Z(1+\delta +it)\right) \le C\log (|t|+2). \]

Proof ▶

Apply Lemma 494 and use Mathlib: Complex.re_le_abs \(\Re (w) \le |w|\) for \(w=\sum _{\rho _1\in \mathcal Z_t} \frac{m_{\rho _1,\zeta }}{1+\delta +it-\rho _1} - Z(1+\delta +it)\).

Lemma 496 Split real

✓

There exists a constant \(C{\gt}0\) such that for all \(0{\lt}\delta {\lt}1\) and \(t\in {\mathbb R}\), we have

\[ \Re \left(\sum _{\rho _1\in \mathcal Z_t} \frac{m_{\rho _1,\zeta }}{1+\delta +it-\rho _1}\right) + \Re \left(- Z(1+\delta +it)\right) \le C\log (|t|+2). \]

Proof ▶

Lemma 497 Double real

✓

There exists a constant \(C{\gt}0\) such that for all \(0{\lt}\delta {\lt}1\) and \(t\in {\mathbb R}\), we have

\[ \Re \left(\sum _{\rho _1\in \mathcal Z_{2t}} \frac{m_{\rho _1,\zeta }}{1+\delta +2it-\rho _1}\right) + \Re \left(-Z(1+\delta +2it)\right) \le C\log (|2t|+2). \]

Proof ▶

Apply Lemma 495 with \(2t\).

Lemma 498 Real sum

✓

If \(\mathcal Z\) is a finite set and \(c_z\in {\mathbb C}\) for \(z\in \mathcal Z\), then \(\Re (\sum _{z\in \mathcal Z}c_{z}) = \sum _{z\in \mathcal Z} \Re (c_{z})\).

Proof ▶

Lemma 499 Sum split

✓

For \(t\in {\mathbb R}\) and \(0{\lt}\delta {\lt}1\), we have

\begin{align*} \Re \Big(\sum _{\rho _1\in \mathcal Z_t} \frac{m_{\rho _1,\zeta }}{1+\delta +it-\rho _1}\Big) = \sum _{\rho _1\in \mathcal Z_t} \Re \Big(\frac{m_{\rho _1,\zeta }}{1+\delta +it-\rho _1}\Big) \end{align*}

Proof ▶

Apply Lemmas 487 and 498 with \(\mathcal Z = \mathcal Z_t\), \(z = \rho _1\), and \(c_{z}=\frac{m_{\rho _1,\zeta }}{1+\delta +it-z}\).

Lemma 500 Sum split

✓

For \(t\in {\mathbb R}\) and \(0{\lt}\delta {\lt}1\), we have

\begin{align*} \Re \Big(\sum _{\rho _1\in \mathcal Z_{2t}} \frac{m_{\rho _1,\zeta }}{1+\delta +2it-\rho _1}\Big) = \sum _{\rho _1\in \mathcal Z_{2t}} \Re \Big(\frac{m_{\rho _1,\zeta }}{1+\delta +2it-\rho _1}\Big) \end{align*}

Proof ▶

Apply Lemma 499 with \(2t\).

Lemma 501 Difference form

✓

For \(\delta {\gt}0\), \(t\in {\mathbb R}\), and \(\rho _1=\sigma _1+it_1\in \mathcal Z_t\) we have

\begin{align*} 1+\delta +it-\rho _1 = (1 + \delta -\sigma _1) + i(t-t_1). \end{align*}

Proof ▶

We calculate \(1+\delta +it-\rho _1 = 1+\delta +it - (\sigma _1+it_1) = (1 + \delta -\sigma _1) + i(t-t_1)\).

Lemma 502 Real part

✓

For \(\delta {\gt}0\), \(t\in {\mathbb R}\), and \(\rho _1=\sigma _1+it_1\in \mathcal Z_t\) we have

\begin{align*} \Re (1+\delta +it-\rho _1) = 1 + \delta -\sigma _1. \end{align*}

Proof ▶

Apply Lemma 501, then take the real part.

Lemma 503 Delta bound

✓

For \(\delta {\gt}0\), \(t\in {\mathbb R}\), and \(\rho _1=\sigma _1+it_1\in \mathcal Z_t\) we have

\begin{align*} 1 + \delta -\sigma _1 \ge \delta . \end{align*}

Proof ▶

Apply Lemma 491.

Lemma 504 Real delta

✓

For \(\delta {\gt}0\), \(t\in {\mathbb R}\), and \(\rho _1=\sigma _1+it_1\in \mathcal Z_t\) we have

\begin{align*} \Re (1+\delta +it-\rho _1) \ge \delta . \end{align*}

Proof ▶

Apply Lemmas 502 and 503.

Lemma 505 Positive real

✓

For \(\delta {\gt}0\), \(t\in {\mathbb R}\), and \(\rho _1=\sigma _1+it_1\in \mathcal Z_t\) we have

\begin{align*} \Re (1+\delta +it-\rho _1) {\gt} 0. \end{align*}

Proof ▶

Apply Lemma 504 and \(\delta {\gt}0\).

Lemma 506 Inverse real

✓

For \(\delta {\gt}0\), \(t\in {\mathbb R}\), and \(\rho _1=\sigma _1+it_1\in \mathcal Z_t\) we have

\begin{align*} \Re \Big(\frac{1}{1+\delta +it-\rho _1}\Big) \ge 0 \end{align*}

Proof ▶

Apply Lemmas 505 and 488 with \(z=1+\delta +it-\rho _1\).

Lemma 507 Scaled real

✓

For \(0{\lt}\delta {\lt}1\), \(t\in {\mathbb R}\), and \(\rho _1=\sigma _1+it_1\in \mathcal Z_t\) we have

\begin{align*} \Re \Big(\frac{m_{\rho _1,\zeta }}{1+\delta +it-\rho _1}\Big) \ge 0 \end{align*}

Proof ▶

Apply lemma 506 and Complex.re_nsmul with \(n=m_{\rho _1,\zeta }\). Note \(m_{\rho _1,\zeta }\in {\mathbb N}\) by 251.

Lemma 508 Double real

✓

For \(0{\lt}\delta {\lt}1\), \(t\in {\mathbb R}\), and \(\rho _1=\sigma _1+it_1\in \mathcal Z_{2t}\) we have

\begin{align*} \Re \Big(\frac{m_{\rho _1,\zeta }}{1+\delta +2it-\rho _1}\Big) \ge 0 \end{align*}

Proof ▶

Apply Lemma 507 with \(2t\).

Lemma 509 Sum nonneg

✓

For \(t\in {\mathbb R}\) and \(0{\lt}\delta {\lt}1\), we have

\begin{align*} \sum _{\rho _1\in \mathcal Z_{2t}} \Re \Big(\frac{m_{\rho _1,\zeta }}{1+\delta +2it-\rho _1}\Big) \ge 0 \end{align*}

Proof ▶

Apply Lemma 508.

Lemma 510 Real nonneg

✓

For \(t\in {\mathbb R}\) and \(0{\lt}\delta {\lt}1\), we have

\begin{align*} \Re \Big(\sum _{\rho _1\in \mathcal Z_{2t}} \frac{m_{\rho _1,\zeta }}{1+\delta +2it-\rho _1}\Big) \ge 0 \end{align*}

Proof ▶

Apply Lemmas 500 and 509.

Lemma 511 Double bound

✓

There exists a constant \(C{\gt}0\) such that for all \(0{\lt}\delta {\lt}1\) and \(t\in {\mathbb R}\), we have

\[ \Re \left(-Z(1+\delta +2it)\right) \le C\log (|2t|+2). \]

Proof ▶

Apply Lemmas 497 and 510.

Lemma 512 Log compare

✓

For \(t\ge 2\) we have \(O(\log (2t)) \le O(\log t)\)

Proof ▶

Apply Lemmas 1 and 4.

Lemma 513 Trivial bound

✓

For \(t\in {\mathbb R}\) we have \(|2t|+2\ge 0\).

Proof ▶

Lemma 514 Log compare

✓

For \(t\in {\mathbb R}\) we have \(O(\log (|2t|+4)) \le O(\log (|t|+2))\)

Proof ▶

Apply Lemmas 513 and 512 with \(w=|t|+2\).

Lemma 515 Shift bound

✓

There exists a constant \(C{\gt}0\) such that for all \(0{\lt}\delta {\lt}1\) and \(t\in {\mathbb R}\), we have

\[ \Re \left(-Z(1+\delta +2it)\right) \le C\log (|t|+2). \]

Proof ▶

Apply Lemmas 511 and 514.

Lemma 516 Split sum

✓

For \(0{\lt}\delta {\lt}1\), \(\sigma , t\in {\mathbb R}\), and \(\rho =\sigma +it\in \mathcal Z\) we have

\begin{align*} \sum _{\rho _1\in \mathcal Z_t} \Re \Big(\frac{m_{\rho _1,\zeta }}{1+\delta +it-\rho _1}\Big) = \Re \Big(\frac{m_{\rho ,\zeta }}{1+\delta +it-\rho }\Big) + \sum _{\rho _1\in \mathcal Z_t, \rho _1 \neq \rho } \Re \Big(\frac{m_{\rho _1,\zeta }}{1+\delta +it-\rho _1}\Big). \end{align*}

Proof ▶

Apply Lemma 527.

Lemma 517 Split bound

✓

For \(0{\lt}\delta {\lt}1\), \(\sigma , t\in {\mathbb R}\), and \(\rho =\sigma +it\in \mathcal Z\) we have

\begin{align*} \sum _{\rho _1\in \mathcal Z_t} \Re \Big(\frac{m_{\rho _1,\zeta }}{1+\delta +it-\rho _1}\Big) \ge \Re \Big(\frac{1}{1+\delta +it-\rho }\Big). \end{align*}

Proof ▶

Apply Lemmas 516 and 506. Note \(m_{\rho _1,\zeta }\ge 1\) by lemma 252.

Lemma 518 Difference real

✓

For \(\delta {\gt}0\), \(\sigma , t\in {\mathbb R}\), and \(\rho =\sigma +it\in \mathcal Z\) we have

\begin{align*} 1+\delta +it-\rho = 1 + \delta -\sigma . \end{align*}

Proof ▶

We calculate \(1+\delta +it-\rho = 1+\delta +it - (\sigma +it) = 1 + \delta -\sigma \).

Lemma 519 Real inverse

✓

For \(0{\lt}\delta {\lt}1\), \(\sigma , t\in {\mathbb R}\), and \(\rho =\sigma +it\in \mathcal Z\) we have

\begin{align*} \Re \Big(\frac{1}{1+\delta +it-\rho }\Big) = \Re \Big(\frac{1}{1 + \delta -\sigma }\Big) \end{align*}

Proof ▶

Apply Lemma 518.

Lemma 520 Inverse real

✓

For \(0{\lt}\delta {\lt}1\), \(\sigma \le 1\) we have \(\frac{1}{1 + \delta -\sigma }\in {\mathbb R}\).

Proof ▶

We calculate \(1+\delta -\sigma \ge \delta {\gt}0\). Thus \(\frac{1}{1 + \delta -\sigma }\in {\mathbb R}\).

Lemma 521 Inverse real

✓

For \(\delta {\gt}0\), \(\sigma , t\in {\mathbb R}\), and \(\rho =\sigma +it\in \mathcal Z\) we have \(\frac{1}{1 + \delta -\sigma }\in {\mathbb R}\).

Proof ▶

Apply Lemmas 490 and 520.

Lemma 522 Real part

✓

For \(x\in {\mathbb R}\) we have \(\Re (x)=x\).

Proof ▶

Lemma 523 Real inverse

✓

For \(\delta {\gt}0\), \(\sigma , t\in {\mathbb R}\), and \(\rho =\sigma +it\in \mathcal Z\) we have

\begin{align*} \Re \Big(\frac{1}{1 + \delta -\sigma }\Big) = \frac{1}{1 + \delta -\sigma } \end{align*}

Proof ▶

Apply Lemmas 521 and 522 with \(x=\frac{1}{1 + \delta -\sigma }\).

Lemma 524 Real inverse

✓

For \(\delta {\gt}0\), \(\sigma , t\in {\mathbb R}\), and \(\rho =\sigma +it\in \mathcal Z\) we have

\begin{align*} \Re \Big(\frac{1}{1+\delta +it-\rho }\Big) = \frac{1}{1 + \delta -\sigma } \end{align*}

Proof ▶

Apply Lemmas 519 and 523

Lemma 525 Sum bound

✓

For \(0{\lt}\delta {\lt}1\), \(\sigma , t\in {\mathbb R}\), and \(\rho =\sigma +it\in \mathcal Z\) we have

\begin{align*} \sum _{\rho _1\in \mathcal Z_t} \Re \Big(\frac{m_{\rho _1,\zeta }}{1+\delta +it-\rho _1}\Big) \ge \frac{1}{1 + \delta -\sigma }. \end{align*}

Proof ▶

Apply Lemmas 517 and 524.

Lemma 526 Real bound

✓

For \(0{\lt}\delta {\lt}1\), \(\sigma , t\in {\mathbb R}\), and \(\rho =\sigma +it\in \mathcal Z\) we have

\begin{align*} \Re \Big(\sum _{\rho _1\in \mathcal Z_t} \frac{m_{\rho _1,\zeta }}{1+\delta +it-\rho _1}\Big) \ge \frac{1}{1 + \delta -\sigma }. \end{align*}

Proof ▶

Apply Lemmas 499 and 525.

Lemma 527 In set

✓

For \(\delta {\gt}0\), \(t\in {\mathbb R}\), let \(\rho =1 + \delta + it\). If \(\rho \in \mathcal Z\), then \(\rho \in \mathcal Z_t\).

Proof ▶

Let \(c=3/2+it\). Then we calculate \(|\rho - c| = |1+\delta - 3/2| = |1/2-\delta | \le 1/2\). And since \(\rho \in \mathcal Z\), we have \(\zeta (\rho )=0\). Thus \(|\rho - c|\le 1/2\) and \(\zeta (\rho )=0\) together imply \(\rho \in \mathcal{Z}_t\).

Lemma 528 Zeta bound

✓

There exists a constant \(C{\gt}1\) such that for all \(0{\lt}\delta {\lt}1\) and \(t\in {\mathbb R}\) and \(\rho =\sigma +it\in \mathcal Z\), we have

\[ \Re \Big(-Z(1+\delta +it)\Big) \le -\frac{1}{1+\delta -\sigma } + C\log (|t|+2). \]

Proof ▶

Apply Lemma 527 so that \(\rho \in \mathcal Z\) implies \(\rho \in \mathcal Z_t\). Then apply 496 and 526.

Lemma 529 At one

✓

For \(\delta {\gt}0\) we have

\[ -Z(1+\delta ) = \frac{1}{\delta } + O(1). \]

Proof ▶

Lemma 530 Real one

✓

For \(\delta {\gt}0\) we have

\[ \Re \Big(-Z(1+\delta )\Big) = \frac{1}{\delta } + O(1). \]

Proof ▶

Apply Lemma 529.

Lemma 531 One bound

✓

There exists a constant \(C{\gt}0\) such that for all \(\delta {\gt}0\) we have

\[ \Big|Z(1+\delta ) - \frac{1}{\delta }\Big| \le C. \]

Proof ▶

By Lemma 529.

Lemma 532 Real bound

✓

There exists a constant \(C{\gt}0\) such that for all \(\delta {\gt}0\) we have

\[ \Re \Big(-Z(1+\delta ) - \frac{1}{\delta }\Big) \le C. \]

Proof ▶

By Lemma 531 and Mathlib Complex.re_le_abs for \(z=Z(1+\delta ) + \frac{1}{\delta }\).

Lemma 533 Real sum

✓

There exists a constant \(C{\gt}0\) such that for all \(\delta {\gt}0\) we have

\[ \Re \big(-Z(1+\delta )\big) + \Re \big(- \frac{1}{\delta }\big) \le C. \]

Proof ▶

By Lemma 532 and Mathlib: Complex.add_re with \(z=-Z(1+\delta )\) and \(w=- \frac{1}{\delta }\).

Lemma 534 Real diff

✓

There exists a constant \(C{\gt}0\) such that for all \(\delta {\gt}0\) we have

\[ \Re \big(-Z(1+\delta )\big) - \frac{1}{\delta } \le C. \]

Proof ▶

By Lemma 533 and Mathlib: RCLike.re_to_real with \(x=1/\delta \), since \(1/\delta \in {\mathbb R}\).

Lemma 535 Combined bound

✓

There exists a constant \(C{\gt}0\) such that for all \(0{\lt}\delta {\lt}1\) and \(t\in {\mathbb R}\) with \(|t|{\gt}3\), if \(\sigma +it\in \mathcal{Z}\) then

\begin{align*} 3\Re \big(& -Z(1+\delta )\big) + 4\Re \big(-Z(1+\delta +it)\big) + \Re \big(-Z(1+\delta +2it)\big) \\ & \le \frac{3}{\delta } - \frac{4}{1+\delta -\sigma } + C\log (|t|+2) \end{align*}

Proof ▶

Apply Lemmas 532 and 528 and 515

Lemma 536 Series form

✓

Let \(s\in {\mathbb C}\). If \({\rm Re}(s){\gt}1\) then

\begin{align*} -Z(s) = \sum _{n=1}^{\infty } \Lambda (n)\, n^{-s} \end{align*}

Proof ▶

Apply definition 484 for \(Z(s)\) and LSeries_vonMangoldt_eq_deriv_riemannZeta_div from Mathlib/NumberTheory/LSeries/Dirichlet.lean

Lemma 537 Series form

✓

For \(x,y\in {\mathbb R}\), if \(x{\gt}1\) then

\begin{align*} -Z(x+iy) = \sum _{n=1}^{\infty } \Lambda (n)\, n^{-(x+iy)} \end{align*}

Proof ▶

Let \(s=x+iy\) so that \({\rm Re}(s)=x{\gt}1\). Apply Lemma 536 with \(s=x+iy\).

Lemma 538 Converges

✓

Let \(x,y\in {\mathbb R}\). If \(x{\gt}1\) then \(Z(x+iy)\) converges.

Proof ▶

Apply definition 484 for \(Z(x+iy)\).

Lemma 539 Real converges

✓

Let \(x,y\in {\mathbb R}\). If \(x{\gt}1\) then \(\Re \big(-Z(x+iy)\big)\) converges.

Proof ▶

Apply Lemma 538.

Lemma 540 Exponent split

✓

For any \(n\ge 1\) and \(x,y\in {\mathbb R}\) we have \(n^{-(x+iy)} = n^{-x} n^{-iy}\).

Proof ▶

Use \(-(x+iy) = -x-iy\), and Lemma 5 with \(\alpha =-x\) and \(\beta =-iy\).

Lemma 541 Series split

✓

For \(x,y\in {\mathbb R}\), if \(x{\gt}1\) then

\begin{align*} -Z(x+iy) = \sum _{n=1}^{\infty } \Lambda (n)\, n^{-x} n^{-iy} \end{align*}

Proof ▶

Apply Lemmas 537 and 540.

Lemma 542 Series converges

✓

Let \(x,y\in {\mathbb R}\). If \(x{\gt}1\) then \(\sum _{n=1}^{\infty } \Lambda (n)\, n^{-x} n^{-iy}\) converges.

Proof ▶

Apply Lemmas 538 and 541.

Lemma 543 Real terms

✓

For \(n,x\ge 1\) we have \(\Lambda (n)\, n^{-x}\ge 0\)

Proof ▶

Proven by definition of von Mangoldt \(\Lambda (n)\ge 0\) and \(n^{-x}\ge 0\).

Lemma 544 Real sum

✓

We have \(\Re \Big(\sum _{n=1}^{\infty } \Lambda (n)\, n^{-x} n^{-iy}\Big) = \sum _{n=1}^{\infty } \Re (\Lambda (n)\, n^{-x} n^{-iy})\)

Proof ▶

Apply Lemmas 542 and 7.

Lemma 545 Series real

✓

For \(x{\gt}1\) and \(y\in {\mathbb R}\), we have \(\Re \big(-Z(x+iy)\big) = \sum _{n=1}^{\infty } \Re (\Lambda (n)\, n^{-x} n^{-iy})\)

Proof ▶

Apply Lemmas 541 and 544.

Lemma 546 Real factor

✓

For \(x{\gt}1\) and \(y\in {\mathbb R}\), we have \(\Re (\Lambda (n)\, n^{-x} n^{-iy}) = \Lambda (n)\, n^{-x}\, \Re (n^{-iy})\).

Proof ▶

Let \(b=\Lambda (n)\, n^{-x}\). By Lemma 543 \(b\in {\mathbb R}\). Apply Lemma 6 with \(b=\Lambda (n)\, n^{-x}\) and \(z=n^{-iy}\).

Lemma 547 Real series

✓

For \(x{\gt}1\) and \(y\in {\mathbb R}\), we have \(\Re \big(-Z(x+iy)\big) = \sum _{n=1}^{\infty } \Lambda (n)\, n^{-x}\, \Re (n^{-iy})\)

Proof ▶

Apply Lemmas 545 and 546.

Lemma 548 Cos form

✓

For \(x{\gt}1\) and \(y\in {\mathbb R}\), \(\Re \big(-Z(x+iy)\big) = \sum _{n=1}^{\infty } \Lambda (n) n^{-x}\cos (y\log n)\).

Proof ▶

Apply Lemmas 547 and 16

Lemma 549 Cos series

✓

For \(x{\gt}1\) and \(y\in {\mathbb R}\), \(\sum _{n=1}^{\infty } \Lambda (n) n^{-x}\cos (y\log n)\) converges.

Proof ▶

Apply Lemmas 539 and 548.

Lemma 550 Double cos

✓

For \(x{\gt}1\) and \(t\in {\mathbb R}\), \(\sum _{n=1}^{\infty } \Lambda (n) n^{-x}\cos (2t\log n)\) converges.

Proof ▶

Apply Lemma 549 with \(y=2t\).

Lemma 551 Zero cos

✓

For \(n\ge 1\), if \(t=0\) then \(\cos (t\log n)=1\).

Proof ▶

For \(t=0\), we calculate \(\cos (t\log n) = \cos (0\log n) = \cos (0)=1\).

Lemma 552 Zero series

✓

For \(x{\gt}1\), \(\sum _{n=1}^{\infty } \Lambda (n) n^{-x}\) converges.

Proof ▶

Apply Lemma 549 with \(y=0\), and Lemma 551.

Lemma 553 Delta series

✓

For \(t\in {\mathbb R}\) and \(\delta {\gt}0\),

\begin{align*} {\rm Re}\Big(-Z(1+\delta +it)\Big) = \sum _{n=1}^{\infty } \Lambda (n) n^{-(1+\delta )}\cos (t\log n) \end{align*}

Proof ▶

Apply Lemma 548 with \(x=1+\delta \) and \(y=t\). Note \(x{\gt}1\) since \(\delta {\gt}0\).

Lemma 554 Delta double

✓

For \(t\in {\mathbb R}\) and \(\delta {\gt}0\), we have

\begin{align*} {\rm Re}\Big(-Z(1+\delta +2it)\Big) = \sum _{n=1}^{\infty } \Lambda (n) n^{-(1+\delta )}\cos (2t\log n) \end{align*}

Proof ▶

Apply Lemma 548 with \(x=1+\delta \) and \(y=2t\). Note \(x{\gt}1\) since \(\delta {\gt}0\).

Lemma 555 Delta zero

✓

Let \(\delta {\gt}0\). We have

\begin{align*} {\rm Re}\Big(-Z(1+\delta )\Big) = \sum _{n=1}^{\infty } \Lambda (n) n^{-(1+\delta )} \end{align*}

Proof ▶

Apply Lemma 548 with \(t=0\), and Lemma 551.

Lemma 556 341 series

✓

For \(t\in {\mathbb R}\) and \(\delta {\gt}0\), we have

\begin{align*} 3& \Re \big(-Z(1+\delta )\big) + 4\Re \big(-Z(1+\delta +it)\big) + \Re \big(-Z(1+\delta +2it)\big)\\ & = 3\sum _{n=1}^{\infty } \Lambda (n) n^{-(1+\delta )} +4\sum _{n=1}^{\infty } \Lambda (n) n^{-(1+\delta )}\cos (t\log n) +\sum _{n=1}^{\infty } \Lambda (n) n^{-(1+\delta )}\cos (2t\log n). \end{align*}

Proof ▶

Apply Lemmas 555 and 553 and 554.

Lemma 557 Sum converges

✓

For \(t\in {\mathbb R}\) and \(\delta {\gt}0\),

\begin{align*} 3 \sum _{n=1}^{\infty } \Lambda (n) n^{-(1+\delta )} +4\sum _{n=1}^{\infty } \Lambda (n) n^{-(1+\delta )}\cos (t\log n) +\sum _{n=1}^{\infty } \Lambda (n) n^{-(1+\delta )}\cos (2t\log n) \end{align*}

converges.

Proof ▶

Apply Lemmas 552 and 549 and 550.

Lemma 558 Factor form

✓

For \(t\in {\mathbb R}\) and \(\delta {\gt}0\), we have

\begin{align*} 3& \sum _{n=1}^{\infty } \Lambda (n) n^{-(1+\delta )} +4\sum _{n=1}^{\infty } \Lambda (n) n^{-(1+\delta )}\cos (t\log n) +\sum _{n=1}^{\infty } \Lambda (n) n^{-(1+\delta )}\cos (2t\log n)\\ & = \sum _{n=1}^{\infty } \Lambda (n) n^{-(1+\delta )}(3 + 4\cos (t\log n) + \cos (2t\log n)). \end{align*}

Proof ▶

Apply Lemmas 552 and 549 and 550.

Lemma 559 Factor conv

✓

For \(t\in {\mathbb R}\) and \(\delta {\gt}0\),

\begin{align*} \sum _{n=1}^{\infty } \Lambda (n) n^{-(1+\delta )}(3 + 4\cos (t\log n) + \cos (2t\log n)) \end{align*}

converges.

Proof ▶

Apply Lemmas 557 and 558.

Lemma 560 Series equal

✓

For \(t\in {\mathbb R}\) and \(\delta {\gt}0\), we have

\begin{align*} 3& \Re \big(-Z(1+\delta )\big) + 4\Re \big(-Z(1+\delta +it)\big) + \Re \big(-Z(1+\delta +2it)\big)\\ & = \sum _{n=1}^{\infty } \Lambda (n) n^{-(1+\delta )}(3 + 4\cos (t\log n) + \cos (2t\log n)). \end{align*}

Proof ▶

Apply Lemmas 556 and 558

Lemma 561 Term nonneg

✓

For \(n\ge 1\), \(\delta {\gt}0\), and \(t\in {\mathbb R}\), we have \(0\le \Lambda (n)\, n^{-(1+\delta )}(3 + 4\cos (t\log n) + \cos (2t\log n))\).

Proof ▶

Apply Lemmas 25 and 543 with \(x=1+\delta \).

Lemma 562 Series nonneg

✓

For \(t\in {\mathbb R}\) and \(\delta {\gt}0\), we have

\[ 0\le \sum _{n=1}^{\infty } \Lambda (n)\, n^{-(1+\delta )}(3 + 4\cos (t\log n) + \cos (2t\log n)) \]

Proof ▶

Apply Lemmas 559, 561, 25, and 26 with \(r_n = \Lambda (n)\, n^{-(1+\delta )}(3 + 4\cos (t\log n) + \cos (2t\log n))\).

Lemma 563 Positive sum

✓

For \(t\in {\mathbb R}\) and \(\delta {\gt}0\), we have

\begin{align*} 0\le 3\Re \big(-Z(1+\delta )\big) + 4\Re \big(-Z(1+\delta +it)\big) + \Re \big(-Z(1+\delta +2it)\big) \end{align*}

Proof ▶

Apply Lemmas 560 and 562.

Lemma 564 Inequality

✓

There exists a constant \(C{\gt}1\) such that, for any \(\sigma +it\in \mathcal{Z}\),

\begin{align*} \frac{4}{1-\sigma +1/(2C\log (|t|+2))}\le 7C\log (|t|+2) \end{align*}

Proof ▶

Apply Lemmas 535 and 563 with \(\delta = 1/(2C\log (|t|+2))\).

Lemma 565 Rearranged

✓

There exists a constant \(C{\gt}0\) such that, for any \(\sigma +it\in \mathcal{Z}\),

\begin{align*} 1-\sigma +1/(2C\log (|t|+2)) \ge 4/(7C\log (|t|+2)) \end{align*}

Proof ▶

Apply Lemma 564.

Lemma 566 Final bound

✓

There exists a constant \(C{\gt}0\) such that, for any \(\sigma +it\in \mathcal{Z}\),

\begin{align*} 1-\sigma \ge 1/(14C\log (|t|+2)) \end{align*}

Proof ▶

Apply Lemma 565.

Lemma 567 Zero free

✓

There exists a constant \(1{\gt}c{\gt}0\) such that if \(\zeta (\sigma +it)=0\) and \(|t|{\gt}3\) for some \(\sigma ,t\in {\mathbb R}\), then \(\sigma \le 1 - \frac{c}{\log (|t|+2)}\).

Proof ▶

Apply Lemma 566 with \(c=1/(14C)\), and Definition 485 of \(\mathcal{Z}\).

4.1 Bound on \(\zeta '/\zeta \)

Definition 568 Delta zeros

✓

For \(t\in {\mathbb R}\) and \(0{\lt}\delta {\lt}1/9\), define

\[ \mathcal{Y}_t(\delta ) = \{ \rho _1\in {\mathbb C}: \zeta (\rho _1) = 0 \, \text{and} \, |\rho _1-(1-\delta +it)|\le 2\delta \} . \]

Definition 569 Delta def

✓

Let \(0{\lt}a{\lt}1\) be the constant in 567. For \(z\in {\mathbb C}\) with \(|\Im (z)|{\gt}2\), define the function \(\delta (z) = \frac{a/20}{\log (|\Im (z)|+2)}\). For \(t\in {\mathbb R}\) define \(\delta _t = \delta (it)\).

Lemma 570 Delta range

✓

For \(z\in {\mathbb C}\) we have \(0{\lt}\delta (z){\lt}1/9\). For \(t\in {\mathbb R}\) we have \(0{\lt}\delta _t{\lt}1/9\).

Proof ▶

Unfold definition 569.

Lemma 571 Zero free

✓

For \(z\in {\mathbb C}\), if \(\Re (z) {\gt} 1 - 9\delta (z)\) then \(\zeta (z)\neq 0\).

Proof ▶

Unfold definition of \(\delta (z)\) in definition 569, and apply contrapositive of lemma 567.

Lemma 572 Disk inclusion

✓

Let \(t\in {\mathbb R}\) with \(|t|{\gt}3\). For \(c=3/2+it\) and \(z=\sigma +it\) with \(1-\delta _t \le \sigma \le 3/2\), we have \(z\in \overline{{\mathbb D}}_{2/3}(c)\).

Proof ▶

We calculate \(|z-c|= |\sigma - 3/2| \le 1/2 + \delta _t\). Note \(\delta _t \le 1/9\) by lemma 570. Hence \(|z-c|\le 2/3\).

Lemma 573 Not zero

✓

Let \(t\in {\mathbb R}\) with \(|t|{\gt}3\). For \(c=3/2+it\) and \(z=\sigma +it\) with \(1-\delta _t \le \sigma \le 3/2\), we have \(z\notin \mathcal K_{\zeta }(5/6;c)\).

Proof ▶

Since \(\Re (z) = \sigma \ge 1-\delta _t = 1 - \delta (z)\), we have \(\zeta (z)\neq 0\) by lemma 571. Thus \(z\notin \mathcal K_{\zeta }(5/6;c)\).

Lemma 574 Expansion

✓

There exists a constant \(C_1{\gt}1\) such that for all \(t\in {\mathbb R}\) with \(|t|{\gt}3\), letting \(c=3/2+it\), and all \(z=\sigma +it\) with \(1-\delta _t \le \sigma \le 3/2\) we have

\begin{align*} \left|\frac{\zeta '(z)}{\zeta (z)} - \sum _{\rho \in \mathcal K_{\zeta }(5/6;c)} \frac{m_{\rho ,\zeta }}{z-\rho } \right| \le C_1\log |t| \end{align*}

Proof ▶

Apply lemma 483 with \(z=\sigma +it\), \(r_1 = 2/3\), \(r = 3/4\), and choosing \(C_1 = C\left(\frac{1}{(r-r_1)^3} + 1\right)\). Note \(z\in \overline{{\mathbb D}}_{r_1}(c)\setminus \mathcal K_\zeta (5/6;c)\) by ??.

Lemma 575 Distance real

✓

For \(z,\rho \in {\mathbb C}\) we have \(|z-\rho | \ge \Re (z) - \Re (\rho )\)

Proof ▶

Apply Mathlib: Complex.re_le_abs and then Complex.sub_re to calculate \(|z-\rho | \ge \Re (z-\rho ) = \Re (z) - \Re (\rho )\).

Lemma 576 Real bound

✓

For \(t\in {\mathbb R}\) with \(|t|{\gt}3\) and \(\rho \in \mathcal K_{\zeta }(5/6;3/2+it)\) we have \(\Re (\rho ) \le 1 - 9\delta (\rho )\).

Proof ▶

By definition \(\rho \in \mathcal K_{\zeta }(5/6;3/2+it)\) implies \(\zeta (\rho )=0\). Then \(\zeta (\rho )=0\) implies \(\Re (\rho ) \le 1 - 9\delta (\rho )\) by the contrapositive of lemma 571.

Lemma 577 Imag bound

✓

For \(t\in {\mathbb R}\) with \(|t|{\gt}3\) and \(z\in \overline{{\mathbb D}}_{5/6}(3/2+it)\), we have \(|\Im (z)| \le |t|+5/6\).

Proof ▶

Unfold definition of \(\overline{{\mathbb D}}_{2\delta _t}(1-\delta _t+it)\).

Lemma 578 Imag growth

✓

For \(t\in {\mathbb R}\) with \(|t|{\gt}3\) and \(z\in \overline{{\mathbb D}}_{5/6}(3/2+it)\), we have \(|\Im (z)|+2 \le (|t|+2)^3\).

Proof ▶

Apply lemma 577 and \(3{\lt}|t|\).

Lemma 579 Log bound

✓

For \(t\in {\mathbb R}\) with \(|t|{\gt}3\) and \(z\in \overline{{\mathbb D}}_{5/6}(3/2+it)\), we have \(\log (|\Im (z)|+2) \le 3\log (|t|+2)\).

Proof ▶

Apply lemma 578 and Mathlib: Real.log_le_log

Lemma 580 Log compare

✓

For \(t\in {\mathbb R}\) with \(|t|{\gt}3\) and \(z\in \overline{{\mathbb D}}_{5/6}(3/2+it)\), we have \(1/\log (|t|+2) \le 3/\log (|\Im (z)|+2)\).

Proof ▶

Apply lemma 579 and Mathlib: one_div_le_one_div

Lemma 581 Delta compare

✓

For \(t\in {\mathbb R}\) with \(|t|{\gt}3\) and \(z\in \overline{{\mathbb D}}_{5/6}(3/2+it)\), we have \(\delta _t \le 3\delta (z)\).

Proof ▶

Unfold definitions of \(\delta _t\) and \(\delta (z)\) from definition 569. Then apply lemma 580.

Lemma 582 Delta bound

✓

Let \(t\in {\mathbb R}\) with \(|t|{\gt}3\), and \(c=3/2+it\). For all \(\rho \in \mathcal K_{\zeta }(5/6;c)\) we have \(\delta (\rho ) \ge \frac{1}{3}\delta _t\)

Proof ▶

Apply lemma 581 with \(z=\rho \). Note \(\mathcal K_{\zeta }(5/6;c)\subset \overline{{\mathbb D}}_{5/6}(c)\).

Lemma 583 Real bound

✓

Let \(t\in {\mathbb R}\) with \(|t|{\gt}3\), and \(c=3/2+it\). For all \(\rho \in \mathcal K_{\zeta }(5/6;c)\) we have \(\Re (\rho ) \le 1 - 3\delta _t\)

Proof ▶

Apply ??.

Lemma 584 Gap bound

✓

Let \(t\in {\mathbb R}\) with \(|t|{\gt}3\), and \(c=3/2+it\). For all \(\rho \in \mathcal K_{\zeta }(5/6;c)\) and \(z=\sigma +it\) with \(1-\delta _t \le \sigma \le 3/2\) we have \(\Re (z) - \Re (\rho ) \ge 2\delta _t\).

Proof ▶

Apply lemma 583, and calculate \(\Re (z) - \Re (\rho ) \ge (1 - \delta _t) - (1 - 3\delta _t) = 2\delta _t\).

Lemma 585 Gap size

✓

Proof ▶

Apply ??

Lemma 586 Nonzero gap

✓

Proof ▶

Apply ??.

Lemma 587 Inverse gap

✓

Proof ▶

Apply lemma 585 and Mathlib: one_div_le_one_div with lemma 570.

Lemma 588 Order nat

✓

For \(t\in {\mathbb R}\) with \(|t|{\gt}3\), let \(c=3/2+it\). Then \(m_{\rho ,\zeta }\in {\mathbb N}\) for all \(\rho \in K_{\zeta }(5/6;c)\).

Proof ▶

Apply ?? with \(\zeta \), \(R_1=5/6\), \(R=8/9\). Note \(\zeta \) AnalyticOnNhd \(\overline{{\mathbb D}}_1(c)\) by lemma 467. Also \(\zeta (c)\neq 0\) by lemma 469

Lemma 589 Finite set

✓

For \(t\in {\mathbb R}\) with \(|t|{\gt}3\), let \(c=3/2+it\). Then \(K_{\zeta }(5/6;c)\) is finite.

Proof ▶

Apply ?? with \(\zeta \), \(R_1=5/6\), \(R=8/9\). Note \(\zeta \) AnalyticOnNhd \(\overline{{\mathbb D}}_1(c)\) by lemma 467. Also \(\zeta (c)\neq 0\) by lemma 469

Lemma 590 Triangle

✓

For all \(t\in {\mathbb R}\) with \(|t|{\gt}3\), letting \(c=3/2+it\), and all \(z=\sigma +it\) with \(1-\delta _t \le \sigma \le 3/2\) we have

\begin{align*} \left|\sum _{\rho \in \mathcal K_{\zeta }(5/6;c)} \frac{m_{\rho ,\zeta }}{z-\rho } \right| \le \sum _{\rho \in \mathcal K_{\zeta }(5/6;c)} \frac{m_{\rho ,\zeta }}{|z-\rho |} \end{align*}

Proof ▶

Apply Mathlib: Finset.abs_sum_le_sum_ab. Note \(\mathcal K_{\zeta }(5/6;c)\) is finite by lemma 589. Then apply Mathlib: abs_div with lemma 586. Note \(m_{\rho ,\zeta }\in {\mathbb N}\) by lemma 588.

Lemma 591 Triangle

✓

There exists a constant \(C_1{\gt}1\) such that for all \(t\in {\mathbb R}\) with \(|t|{\gt}3\), letting \(c=3/2+it\), and all \(z=\sigma +it\) with \(1-\delta _t \le \sigma \le 3/2\) we have

\begin{align*} \Big|\frac{\zeta '(z)}{\zeta (z)}\Big| \le \sum _{\rho \in \mathcal K_{\zeta }(5/6;c)} \frac{m_{\rho ,\zeta }}{|z-\rho |} + C_1\log |t| \end{align*}

Proof ▶

Apply ??.

Lemma 592 Sum bound

✓

For all \(t\in {\mathbb R}\) with \(|t|{\gt}3\), letting \(c=3/2+it\), and all \(z=\sigma +it\) with \(1-\delta _t \le \sigma \le 3/2\) we have

\[ \sum _{\rho \in \mathcal K_{\zeta }(5/6;c)} \frac{m_{\rho ,\zeta }}{|z-\rho |} \le \frac{1}{2\delta _t}\sum _{\rho \in \mathcal K_{\zeta }(5/6;c)}m_{\rho ,\zeta } \]

Proof ▶

Apply lemma 587.

Lemma 593 Order bound

✓

Let \(B{\gt}1\), \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1(c)\). If \(f(c)\neq 0\) and \(|f(z)|\le B\) on \(z\in \overline{{\mathbb D}}_R(c)\), then \(\sum _{\rho \in \mathcal K_f(R_1;c)} m_{\rho ,f} \le \frac{\log (B/|f(c)|)}{\log (R/R_1)}\).

Proof ▶

Use the conditions from ?? with \(f=\zeta \), and then apply lemma 324 with \(\zeta _c(z) = \zeta (z+c)/\zeta (c)\). Note \(\zeta \) is AnalyticOnNhd \(\overline{{\mathbb D}}_1(c)\) by lemma 467. Also \(\zeta (c)\neq 0\) by lemma 469.

Lemma 594 Order sum

✓

There exists a constant \(C_2{\gt}1\) such that for all \(t\in {\mathbb R}\) with \(|t|{\gt}3\), letting \(c=3/2+it\), we have \(\sum _{\rho \in \mathcal K_{\zeta }(5/6;c)}m_{\rho ,\zeta } \le C_2 \log |t|\)

Proof ▶

Apply lemma 593 with \(R_1=5/6\), \(R=8/9\). Then by lemma 481, we set \(B = b|t|\). Thus \(\log (B/|f(c)|) \le \log |t| + \log (b/|f(c)|)\). Thus we may choose \(C_2 = 2(1+\log (b/|f(c)|))/\log (R/R_1)\).

Lemma 595 Sum bound

✓

There exists a constant \(C_3{\gt}1\) such that for all \(t\in {\mathbb R}\) with \(|t|{\gt}3\), letting \(c=3/2+it\), and all \(z=\sigma +it\) with \(1-\delta _t \le \sigma \le 3/2\) we have

\[ \sum _{\rho \in \mathcal K_{\zeta }(5/6;c)} \frac{m_{\rho ,\zeta }}{|z-\rho |} \le \frac{C_3}{\delta _t} \log |t| \]

Proof ▶

Apply ??.

Lemma 596 Sum bound

✓

There exists a constant \(C_4{\gt}1\) such that for all \(t\in {\mathbb R}\) with \(|t|{\gt}3\), letting \(c=3/2+it\), and all \(z=\sigma +it\) with \(1-\delta _t \le \sigma \le 3/2\) we have

\[ \sum _{\rho \in \mathcal K_{\zeta }(5/6;c)} \frac{m_{\rho ,\zeta }}{|z-\rho |} \le C_4\log |t|^2 \]

Proof ▶

Apply ??.

Lemma 597 Log bound

✓

There exists a constant \(C{\gt}1\) such that for all \(t\in {\mathbb R}\) with \(|t|{\gt}3\), and all \(s=\sigma +it\) with \(1-\delta _t \le \sigma \le 3/2\), we have

\[ \Big|\frac{\zeta '}{\zeta }(s)\Big| \le C\log |t|^2 \]

Proof ▶

Apply ??.

Lemma 598 Log bound

✓

There exist constants \(0{\lt}A{\lt}1\) and \(C{\gt}1\) such that for all \(t\in {\mathbb R}\) with \(|t|{\gt}3\), and all \(s=\sigma +it\) with \(1 - A/\log (|t|+2) \le \sigma \le 3/2\), we have

\[ \Big|\frac{\zeta '}{\zeta }(s)\Big| \le C\log |t|^2 \]

Proof ▶

Apply ??.

Lemma 599 Real bound

✓

Let \(t\in {\mathbb R}\). If \(z\in \overline{{\mathbb D}}_{2\delta _t}(1-\delta _t+it)\) then \(\Re (z) {\gt} 1-4\delta _t\)

Proof ▶

Apply lemma 612 with \(\delta =\delta _t\).

Lemma 600 Real bound

✓

For \(t\in {\mathbb R}\) with \(|t|{\gt}3\) and \(z\in \overline{{\mathbb D}}_{2\delta _t}(1-\delta _t+it)\), we have \(\Re (z) \ge 1 - 6\delta (z)\)

Proof ▶

Apply ??.

Lemma 601 In disk

✓

For \(t\in {\mathbb R}\) with \(|t|{\gt}3\) we have \(\mathcal{Y}_t(\delta _t)\subset \overline{{\mathbb D}}_{2\delta _t}(1-\delta _t+it)\).

Proof ▶

Unfold definition of \(\mathcal{Y}_t(\delta _t)\) in definition 568

Lemma 602 Zero set

✓

Let \(t\in {\mathbb R}\) and \(\delta {\gt}0\). If \(\rho _1\in \mathcal{Y}_t(\delta )\) then \(\zeta (\rho _1) = 0\).

Proof ▶

Unfold definition 568 for \(\mathcal{Y}_t(\delta )\).

Lemma 603 Real abs

✓

For \(w\in {\mathbb C}\) we have \(|\Re (w)| \le |w|\)

Proof ▶

Mathlib (try Complex.abs_re_le_abs)

Lemma 604 Real diff

✓

Let \(t\in {\mathbb R}\), \(1/9 {\gt} \delta {\gt}0\) and \(z\in {\mathbb C}\). Then \(|\Re (z-(1-\delta +it))| \le |z-(1-\delta +it)|\)

Proof ▶

Apply Lemma 603 with \(w=z-(1-\delta +it)\).

Lemma 605 Real diff

✓

Let \(t\in {\mathbb R}\), \(1/9 {\gt} \delta {\gt}0\) and \(z\in {\mathbb C}\). If \(|z-(1-\delta +it)| \le \delta /2\) then \(|\Re (z-(1-\delta +it))| \le \delta /2\).

Proof ▶

Apply Lemma 604.

Lemma 606 Real diff

✓

Let \(t\in {\mathbb R}\) and \(1/9 {\gt} \delta {\gt}0\) and \(z\in {\mathbb C}\). We have \(\Re (z-(1-\delta +it)) = \Re (z)-(1-\delta )\)

Proof ▶

Lemma 607 Real diff

✓

Let \(t\in {\mathbb R}\), \(1/9 {\gt} \delta {\gt}0\) and \(z\in {\mathbb C}\). If \(|z-(1-\delta +it)| \le \delta /2\) then \(|\Re (z)-(1-\delta )| \le \delta /2\)

Proof ▶

Apply Lemmas 605 and 606.

Lemma 608 Neg bound

✓

Let \(a\in {\mathbb R}\) and \(b{\gt}0\). If \(|a|\le b\) then \(a\ge -b\).

Proof ▶

Mathlib (try neg_le_of_abs_le)

Lemma 609 Real bound

✓

Let \(1/ 9 {\gt} \delta {\gt}0\) and \(z\in {\mathbb C}\). If \(|\Re (z)-(1-\delta )| \le \delta /2\) then \(\Re (z)-(1-\delta ) \ge -\delta /2\)

Proof ▶

608 with \(a=\Re (z)-(1-\delta )\) and \(b=\delta /2\).

Lemma 610 Real bound

✓

Let \(0{\lt}\delta {\lt}1/9\) and \(z\in {\mathbb C}\). If \(|\Re (z)-(1-\delta )| \le 2\delta \) then \(\Re (z) \ge 1-3\delta \)

Proof ▶

Apply Lemma 609 and then add \(1-\delta \) to both sides.

Lemma 611 Real bound

✓

Let \(0{\lt}\delta {\lt}1/9\) and \(z\in {\mathbb C}\). If \(|\Re (z)-(1-\delta )| \le 2\delta \) then \(\Re (z) {\gt} 1-4\delta \)

Proof ▶

Apply Lemma 610, and then use \(1-\frac{3}{2}\delta {\gt} 1-2\delta \), since \(\delta {\gt}0\).

Lemma 612 Real bound

✓

Let \(t\in {\mathbb R}\), \(0{\lt}\delta {\lt}1/9\) and \(z\in {\mathbb C}\). If \(|z-(1-\delta +it)| \le 2\delta \) then \(\Re (z) {\gt} 1-4\delta \).

Proof ▶

Apply Lemmas 607 and 611.

Lemma 613 Empty set

✓

For \(t\in {\mathbb R}\) with \(|t|{\gt}3\) we have \(\mathcal{Y}_t(\delta _t)= \emptyset \).

Proof ▶

Lemma 614 Empty sum

✓

For any \(g:{\mathbb C}\to {\mathbb C}\), if \(S=\emptyset \) then

\begin{align*} \sum _{s\in S}g(s) = 0 \end{align*}

Proof ▶

Mathlib (try Mathlib.Meta.NormNum.Finset.sum_empty)

Lemma 615 Zero sum

✓

For \(t\in {\mathbb R}\) with \(|t|{\gt}3\) we have

\begin{align*} \sum _{\rho _1\in \mathcal{Y}_t(\delta _t)} \frac{m_{\rho _1,\zeta }}{1-\delta _t+it-\rho _1} = 0. \end{align*}

Proof ▶

Apply Lemmas 613 and 614 with \(g(s) = \frac{m_{\rho _1,\zeta }}{1-\delta _t+it-s}\) and \(S=\mathcal{Y}_t(\delta _t)\).

Lemma 616 Center bound

✓

For \(\sigma \ge 3/2\) and \(t\in {\mathbb R}\) we have \(|\frac{\zeta '}{\zeta }(\sigma + it)| \le |\frac{\zeta '}{\zeta }(\sigma )|\)

Proof ▶

By Mathlib: ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div

we have \(-\frac{\zeta '}{\zeta }(\sigma + it) = \sum _{n=1}^\infty \frac{\Lambda (n)}{n^s}\).

Note this series is summable by Mathlib: ArithmeticFunction.LSeriesSummable_vonMangoldt

Then apply Mathlib: norm_tsum_le_tsum_norm so that \(|\frac{\zeta '}{\zeta }(\sigma + it)| \le \sum _{n=1}^\infty \frac{\Lambda (n)}{|n^s|}\).

Observe \(|n^s| = n^{\Re (s)}e^{-\operatorname{Arg}(s)\Im (n)}\) by Mathlib: Complex.abs_cpow_le. Note \(n\in {\mathbb R}\) so \(\Im (n)=0\) by imaginaryPart_ofReal. Thus \(e^{-\operatorname{Arg}(s)\Im (n)} = e^0 = 1\). And \(\Re (s)=\sigma \). Hence \(|n^s| = n^{\sigma }\).

Thus \(|\frac{\zeta '}{\zeta }(\sigma + it)| \le \sum _{n=1}^\infty \frac{\Lambda (n)}{n^\sigma }\).

Again by Mathlib: ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div we have\(\sum _{n=1}^\infty \frac{\Lambda (n)}{n^\sigma } = -\frac{\zeta '}{\zeta }(\sigma )\).

Take absolute values to get \(|\frac{\zeta '}{\zeta }(\sigma + it)| \le |\frac{\zeta '}{\zeta }(\sigma )|\).

Lemma 617 Log bound

✓

There exists a constant \(C{\gt}1\) such that for all \(t\in {\mathbb R}\) with \(|t|{\gt}3\), and all \(s=\sigma +it\) with \(\sigma \ge 3/2\), we have

\[ \Big|\frac{\zeta '}{\zeta }(s)\Big| \le C \]

Proof ▶

Apply lemma 616 and then lemma 531.

Theorem 618 Bound on \(\zeta '/\zeta \)

✓

There exist constants \(0{\lt}A{\lt}1\) and \(C{\gt}1\) such that for any \(t\in {\mathbb R}\) with \(|t|{\gt}3\) and \(\sigma \ge 1 - A/\log (|t|+2)\), we have

\[ \left|\frac{\zeta '}{\zeta }(\sigma + it)\right| \le C\log |t|^2. \]

Proof ▶

Apply ??

Lemma 619 Zero-free region near 1

✓

There exists a constant \(A\in (0,\tfrac 12)\) such that for every real \(t\) with \(|t|{\gt}3\) and every real \(\sigma \) with

\[ \sigma \in [1 - A/\log |t|,\; 1), \]

we have

\[ \zeta (\sigma + i t) \neq 0. \]

In other words, a uniform zero-free region of the form \(\Re s \ge 1 - A/\log |\Im s|\) holds for large \(|\Im s|\).

Proof ▶

Lemma 620 Uniform bound on the logarithmic derivative of \(\zeta \)

✓

There exist constants \(A\in (0,\tfrac 12)\) and \(C{\gt}0\) such that for every real \(t\) with \(|t|{\gt}3\) and every real \(\sigma \) with

\[ \sigma \ge 1 - A/\log |t|, \]

the logarithmic derivative of the Riemann zeta function satisfies the uniform bound

\[ \left|\frac{\zeta '(\sigma + i t)}{\zeta (\sigma + i t)}\right| \le C\, \log |t|^2. \]

The constants \(A,C\) are absolute (independent of \(\sigma \) and \(t\)) and give a uniform control of \(\zeta '/\zeta \) in the stated region.

Proof ▶