Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized
Dark green border: this is in Mathlib

Definition 90Open disk

For \(R{\gt}0\), define the open ball \({\mathbb D}_R := \{ z\in {\mathbb C}: |z| {\lt} R\} \).

LaTeX Lean

Definition 275Blaschke B

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)\neq 0\). Define the function \(B_f:\overline{{\mathbb D}}_R\to {\mathbb C}\) as \(B_f(z)=C_f(z)\prod _{\rho \in \mathcal K_f(R_1)} (R-\bar\rho z/R)^{m_{\rho ,f}}\).

LaTeX Lean

Definition 257C function

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)\neq 0\). We define the function \(C_f:\overline{{\mathbb D}}_R\to {\mathbb C}\) as follows. This function is constructed by dividing \(f(z)\) by a polynomial whose roots are the zeros of \(f\) inside \(\overline{{\mathbb D}}_{R_1}\). The definition is split into two cases to handle the points where the denominator would otherwise be zero.

\[ C_f(z) = \begin{cases} \displaystyle \frac{f(z)}{\prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}}} & \text{if } z \neq \rho \text{ for all } \rho \in \mathcal{K}_f(R_1) \\ \displaystyle \frac{h_\sigma (\sigma )}{\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(\sigma -\rho )^{m_{\rho ,f}}} & \text{if } z = \sigma \text{ for some } \sigma \in \mathcal{K}_f(R_1) \end{cases} \]

LaTeX

Definition 569Delta 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)\).

LaTeX

Lean

deltaz
deltaz_t

Definition 117Modified function

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). Define the function \(f_M(z)\) for \(|z| \le R\) as

\[ f_M(z) = \frac{f(z)/z}{2M - f(z)}. \]

LaTeX Lean

Definition 221Auxiliary function

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Define \(J(z) := I_{B'/B}(z)\) from lemma 220. Define \(H(z) := \exp (J(z))/B(z)\).

LaTeX Lean

Definition 200Integral along the taxicab path

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Define the function \(I_f:\overline{{\mathbb D}}_R\to \mathbb {C}\) by

\[ I_f(z) := \int _0^{z.\operatorname {Re}} f(t)\, dt + i \int _0^{z.\operatorname {Im}} f(z.\operatorname {Re}+ i\tau )\, d\tau . \]

LaTeX Lean

Definition 330Log function

Let \(0{\lt}R{\lt}1\), \(B{\gt}1\), and \(f:{\mathbb C}\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). Define \(L_f(z) = J_{B_f}(z)\) from lemma 238, where \(B_f\) from definition 275.

LaTeX

Definition 484Log derivative

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

LaTeX Lean

Definition 250Zero order

Let \(0{\lt}R_1{\lt}1\) and \(f:{\mathbb C}\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\). For any zero \(\rho \in \mathcal K_f(R_1)\) of the function \(f\), we define \(m_{\rho ,f}\) as the analytic order of \(f\) at \(\rho \), denoted by analyticOrderAt \(f\) \(\rho \).

LaTeX

Definition 384Prime set

Let \(\mathcal{P}\) be Nat.Primes

LaTeX

Definition 568Delta 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 \} . \]

LaTeX Lean

Definition 486Window 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\} \]

LaTeX Lean

Definition 240Zero set

Let \(R{\gt}0\) and \(f:\overline{{\mathbb D}}_R\to {\mathbb C}\). Define the set of zeros \(\mathcal{K}_f(R) = \{ \rho \in {\mathbb C}: |\rho | \le R \text{ and } f(\rho )=0\} \).

LaTeX Lean

Definition 485Zero set

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

LaTeX Lean

Definition 416Partial sum

For \(s\in {\mathbb C}\) and \(N\in {\mathbb N}\), define the partial sum \(\zeta _N(s) = \sum _{n=1}^N n^{-s}\).

LaTeX Lean

Lemma 520Inverse real

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

LaTeX Lean

Lemma 521Inverse 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}\).

LaTeX Lean

Lemma 587Inverse gap

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 \(\frac{1}{|z-\rho |} \le \frac{1}{2\delta _t}\).

LaTeX Lean

Lemma 345One minus B

Let \(0{\lt}R{\lt}1\) and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). Then \(B_f(0)\neq 0\) and \(1/B_f(0)\neq 0\).

LaTeX Lean

Lemma 519Real 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*}

LaTeX Lean

Lemma 523Real 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*}

LaTeX Lean

Lemma 524Real 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*}

LaTeX Lean

Lemma 518Difference 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*}

LaTeX Lean

Lemma 501Difference 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*}

LaTeX Lean

Lemma 75Inverse analytic

The function \(f_1(z) = \frac{1}{z}\) is analytic on \(\{ z\in {\mathbb C}: z \neq 0\} \).

LaTeX

Lemma 78Inverse analytic

The function \(f_1(z) = \frac{1}{z}\) is analytic on \(T=\{ z\in \overline{{\mathbb D}}_R: z \neq 0\} \).

LaTeX Lean

Lemma 1Log growth

For \(t{\gt} 1\) we have \(2\log t \le O(\log t)\)

LaTeX Lean

Lemma 190Double positive

Given \(0 {\lt} R\), we have \(2R {\gt} 0\).

LaTeX Lean

Lemma 193Square identity

For any \(R{\gt}0\), we have \((2R)^2 = 4R^2\).

LaTeX Lean

Lemma 558Factor 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*}

LaTeX Lean

Lemma 560Series 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*}

LaTeX Lean

Lemma 557Sum 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.

LaTeX Lean

Lemma 559Factor 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.

LaTeX Lean

Lemma 564Inequality

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*}

LaTeX Lean

Lemma 565Rearranged

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*}

LaTeX Lean

Lemma 566Final 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*}

LaTeX Lean

Lemma 563Positive 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*}

LaTeX Lean

Lemma 556341 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*}

LaTeX Lean

Lemma 323Three exceeds e

We have \(3 {\gt} \exp (1)\).

LaTeX Lean

Lemma 64Double positive

For \(a\in {\mathbb R}\), if \(a{\gt}0\) then \(2a{\gt}0\).

LaTeX Lean

Lemma 417Abel sum

Let \(a_n \in {\mathbb C}\) and let \(f: {\mathbb R}\to {\mathbb C}\) be a continuously differentiable function. Let \(A(u) = \sum _{n=1}^{\lfloor u \rfloor } a_n\). Then for any integer \(N\ge 1\),

\[ \sum _{n=1}^N a_n f(n) = A(N)f(N) - \int _1^N A(u) f'(u) du. \]

LaTeX Lean

Lemma 390Abs inverse

For \(z\in {\mathbb C}\), if \(z\neq 0\) then \(|z^{-1}| = |z|^{-1}\).

LaTeX Lean

Lemma 387Abs product

Let \(P\) be a set and \(w:P\to {\mathbb C}\) be multipliable. Then \(|\prod '_{p\in P} w(p)| = \prod '_{p \in P} |w(p)|\).

LaTeX Lean

Lemma 404Prime power

For \(p\in \mathcal{P}\) and \(s=\sigma +it \in {\mathbb C}\), we have \(|p^{-s}| = p^{-\sigma }\).

LaTeX Lean

Lemma 388Abs primes

For \(s\in {\mathbb C}\) with \(\Re (s){\gt}1\), we have \(|\prod '_{p\in \mathcal{P}}(1-p^{-s})^{-1}| = \prod '_{p\in \mathcal{P}}|(1-p^{-s})^{-1}|\).

LaTeX Lean

Lemma 295Abs power

For \(n\in {\mathbb N}\) and \(w\in {\mathbb C}\), we have \(|w^n|=|w|^n\).

LaTeX Lean

Lemma 405Term bound

For \(p\in \mathcal{P}\) and \(t\in {\mathbb R}\), we have \(|1 - p^{-(3/2+it)}| \le 1 + p^{-3/2}\).

LaTeX Lean

Lemma 408Inverse bound

For \(p\in \mathcal{P}\) and \(t\in {\mathbb R}\), we have \(|1 - p^{-(3/2+it)}|^{-1} \ge (1 + p^{-3/2})^{-1}\).

LaTeX Lean

Lemma 410Zeta compare

For \(t\in {\mathbb R}\), we have \(\prod '_{p\in \mathcal{P}}(1 + p^{-3/2})^{-1} \le \prod '_{p\in \mathcal{P}}|1 - p^{-(3/2+it)}|^{-1}\).

LaTeX Lean

Lemma 389Abs zeta

For \(s\in {\mathbb C}\) with \(\Re (s){\gt}1\), we have \(|\zeta (s)| = \prod '_{p\in \mathcal{P}}|(1-p^{-s})^{-1}|\).

LaTeX Lean

Lemma 392Abs product

For \(s\in {\mathbb C}\) with \(\Re (s){\gt}1\), we have \(|\zeta (s)| = \prod '_{p\in \mathcal{P}}|1-p^{-s}|^{-1}\).

LaTeX Lean

Lemma 119Quotient modulus

Let \(a,b\in {\mathbb C}\). If \(b\neq 0\) then \(|a/b| = |a|/|b|\).

LaTeX Lean

Lemma 165Division bound

If \(a,b\in {\mathbb C}\) and \(b\neq 0\) then \(|a/b|=|a|/|b|\).

LaTeX Lean

Lemma 35Absolute value positive

Let \(z\in {\mathbb C}\). If \(z\neq 0\) then \(|z|{\gt}0\).

LaTeX Lean

Lemma 63Abs positive

For \(a\in {\mathbb R}\), if \(a{\gt}0\) then \(|a|=a\).

LaTeX Lean

Lemma 65Scaled abs

For \(a\in {\mathbb R}\), if \(a{\gt}0\) then \(|2a|=2a\).

LaTeX Lean

Lemma 603Real abs

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

LaTeX Lean

Lemma 609Real 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\)

LaTeX Lean

Lemma 610Real 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 \)

LaTeX Lean

Lemma 611Real 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 \)

LaTeX Lean

Lemma 585Gap size

LaTeX Lean

Lemma 586Nonzero gap

LaTeX Lean

Lemma 575Distance real

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

LaTeX Lean

Lemma 89Local to global

Let \(T=\{ z\in \ \overline{{\mathbb D}}_R : z\neq 0\} \) and \(h: {\mathbb C}\to {\mathbb C}\). If \(h\) is AnalyticAt \(0\) and \(h\) is AnalyticOn \(T\), then \(h\) is AnalyticOn \(\overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 88At to within

Let \(h:{\mathbb C}\to {\mathbb C}\). If \(h\) is AnalyticAt \(0\), then \(h\) is AnalyticWithinAt \(0\).

LaTeX Lean

Lemma 102Analytic Continuation

If \(h:\overline{{\mathbb D}}_R \to {\mathbb C}\) is analytic, then \(h\) is continuous.

LaTeX Lean

Lemma 253Analytic division

Let \(D \subset {\mathbb C}\) be an open set, and let \(w\in D\). Let \(h:D\to {\mathbb C}\) and \(g:D\to {\mathbb C}\) be functions that are analyticAt \(w\). If \(g(w)\neq 0\), then the function \(z \mapsto h(z)/g(z)\) is analyticAt \(w\).

LaTeX Lean

Lemma 76Analytic mono

Let \(T\subset S\subset {\mathbb C}\) and \(f:S\to {\mathbb C}\). If \(f\) is analytic on \(S\) then \(f\) is analytic on \(T\).

LaTeX Lean

Lemma 83On implies within

Let \(V\subset {\mathbb C}\) and \(h:{\mathbb C}\to {\mathbb C}\). If \(h\) is AnalyticOn \(V\), then \(h\) is AnalyticWithinAt \(z\) for all \(z\in V\).

LaTeX Lean

Lemma 79Product analytic

Let \(T\subset S\subset {\mathbb C}\), and let \(f_1:S\to {\mathbb C}\) and \(f_2:S\to {\mathbb C}\). If \(f_1\) is analytic on \(T\) and \(f_2\) is analytic on \(T\), then \(f_1\cdot f_2\) is analytic on \(T\).

LaTeX Lean

Lemma 80Product analytic

Let \(T\subset S\subset {\mathbb C}\), and let \(f_1:S\to {\mathbb C}\) and \(f_2:S\to {\mathbb C}\). If \(f_1\) is analytic on \(T\) and \(f_2\) is analytic on \(S\), then \(f_1\cdot f_2\) is analytic on \(T\).

LaTeX Lean

Lemma 81Product analytic

Let \(T=\{ z\in \ \overline{{\mathbb D}}_R : z\neq 0\} \) and \(f_1:{\mathbb C}\to {\mathbb C}\) and \(f_2:{\mathbb C}\to {\mathbb C}\). If \(f_1\) is analytic on \(T\) and \(f_2\) is analytic on \(\overline{{\mathbb D}}_R\), then \(f_1\cdot f_2\) is analytic on \(T\).

LaTeX Lean

Lemma 84Within implies on

Let \(h:{\mathbb C}\to {\mathbb C}\). If \(h\) is AnalyticWithinAt \(z\) for all \(z\in \overline{{\mathbb D}}_R\), then \(h\) is AnalyticOn \(\overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 87Within gives on

Let \(T=\{ z\in \ \overline{{\mathbb D}}_R : z\neq 0\} \) and \(h: {\mathbb C}\to {\mathbb C}\). If \(h\) is AnalyticWithinAt \(0\) and \(h\) is AnalyticWithinAt \(z\) for all \(z\in T\), then \(h\) is AnalyticOn \(\overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 86Within union

LaTeX Lean

Lemma 232Existence of analytic logarithm

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) with \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). For \(J\) from lemma 220, then \(B(z) = B(0)\exp (J(z))\) for all \(z \in \overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 256Zero factorization

Let \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)\neq 0\). For each \(\sigma \in \mathcal{K}_f(R_1)\), there exists a function \(h_\sigma (z)\) that is AnalyticAt \(\sigma \), and \(h_\sigma (\sigma ) \neq 0\), and \(f(z) = (z-\sigma )^{m_{\sigma ,f}} h_\sigma (z)\) Eventually for \(z\) in nbhds of \(\sigma \).

LaTeX Lean

Lemma 343Apply BC

Let \(B{\gt}1\), \(0{\lt} r_1 {\lt} r{\lt}R_1{\lt}R{\lt}1\) and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\). If \(f(0)=1\) and \(|f(z)|\le B\) on \(|z|\le R\). For any \(|z|\le r_1\)

\[ |L_f'(z)| \le \frac{16\log (B) r^2}{(r-r_1)^3}. \]

LaTeX Lean

Lemma 421Apply Abel

For \(s\in {\mathbb C}\) and integer \(N\ge 1\),

\[ \zeta _N(s) = \lfloor N \rfloor N^{-s} - \int _1^N \lfloor u \rfloor (-s u^{-s-1}) du. \]

LaTeX Lean

Lemma 91Disk closure

For \(R{\gt}0\), the closure of \({\mathbb D}_R\) equals \(\overline{{\mathbb D}}_R := \{ z\in {\mathbb C}: |z|\le R\} \)

LaTeX Lean

Lemma 132BC bound

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(0{\lt}r {\lt} R\), and any \(z\in {\mathbb C}\) with \(|z|\le r\) we have

\[ |f(z)| \le \frac{2r}{R-r}M. \]

LaTeX Lean

Lemma 342BC inequality

Let \(M{\gt}0\) and \(0{\lt}r_1{\lt}r{\lt}1\). Let \(L\) be analytic on \(|z| \le r\) such that \(L(0)=0\) and suppose \(\Re (L(z)) \le M\) for all \(|z| \le r\). Then for any \(|z|\le r_1\),

\[ |L'(z)| \le \frac{16M r^2}{(r-r_1)^3}. \]

LaTeX Lean

Lemma 333B zero

Let \(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\). Then \(B_f(0) \neq 0\).

LaTeX Lean

Lemma 318Zero bound

Let \(B{\gt}1\), \(0{\lt}R{\lt}1\) and \(f:{\mathbb C}\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\). If \(|f(z)|\le B\) on \(|z|\le R\), then \(|B_f(0)|\le B\).

LaTeX Lean

Lemma 316Disk bound

Let \(B{\gt}1\), \(0{\lt}R{\lt}1\) and \(f:{\mathbb C}\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\). If \(|B_f(z)|\le B\) for all \(|z|=R\), then \(|B_f(z)|\le B\) for all \(|z|\le R\).

LaTeX Lean

Lemma 317Disk bound

Let \(B{\gt}1\), \(0{\lt}R{\lt}1\) and \(f:{\mathbb C}\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\). If \(|f(z)|\le B\) on \(|z|\le R\), then \(|B_f(z)|\le B\) for all \(|z|\le R\).

LaTeX Lean

Lemma 314Boundary bound

Let \(B{\gt}1\), \(0{\lt}R{\lt}1\) and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\). If \(|f(z)|\le B\) on \(|z|\le R\) then \(|B_f(z)|\le B\) for all \(|z|=R\).

LaTeX Lean

Lemma 357Outside zeros

Let \(0{\lt}R{\lt}1\), \(R_1=\frac{2}{3}R\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). Then the function \(B_f(z)\) is never equal to zero, and differentiableAt \(z\) for all \(z\in \overline{{\mathbb D}}_{R_1}\setminus \mathcal K_f(R_1)\).

LaTeX Lean

Lemma 277B division

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)\neq 0\). For \(z\in \overline{{\mathbb D}}_R\setminus \mathcal K_f(R_1)\), we have

\begin{align*} \frac{\prod _{\rho \in \mathcal K_f(R_1)} (R-\bar\rho z/R)^{m_{\rho ,f}}}{\prod _{\rho \in \mathcal K_f(R_1)} (z-\rho )^{m_{\rho ,f}}} = \prod _{\rho \in \mathcal K_f(R_1)}\frac{ (R-\bar\rho z/R)^{m_{\rho ,f}}}{(z-\rho )^{m_{\rho ,f}}} \end{align*}

LaTeX Lean

Lemma 312B analytic

Let \(0{\lt}R_1{\lt}R{\lt}1\) and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)\neq 0\). Then \(B_f(z)\) is AnalyticOnNhd \(\overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 331Disk analytic

Let \(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\). Then \(B_f(z)\) is AnalyticOnNhd \(\overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 332Never zero

Let \(0{\lt}R_1{\lt}R{\lt}1\) and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\). Then \(B_f(z) \neq 0\) for all \(z \in \overline{{\mathbb D}}_{R_1}\).

LaTeX Lean

Lemma 279B off K

\begin{align*} B_f(z)= f(z)\prod _{\rho \in \mathcal K_f(R_1)} \left(\frac{R-\bar\rho z/R}{z-\rho } \right)^{m_{\rho ,f}}. \end{align*}

LaTeX Lean

Lemma 278B product pow

\begin{align*} \prod _{\rho \in \mathcal K_f(R_1)}\frac{ (R-\bar\rho z/R)^{m_{\rho ,f}}}{(z-\rho )^{m_{\rho ,f}}}= \prod _{\rho \in \mathcal K_f(R_1)} \left(\frac{R-\bar\rho z/R}{z-\rho } \right)^{m_{\rho ,f}} \end{align*}

LaTeX Lean

Lemma 276B and C relation

\begin{align*} B_f(z)= f(z) \frac{\prod _{\rho \in \mathcal K_f(R_1)} (R-\bar\rho z/R)^{m_{\rho ,f}}}{\prod _{\rho \in \mathcal K_f(R_1)} (z-\rho )^{m_{\rho ,f}}} \end{align*}

LaTeX Lean

Lemma 273Blaschke diff

Let \(0{\lt}R_1{\lt}R{\lt}1\) and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). Then the function \(z \mapsto \prod _{\rho \in \mathcal K_f(R_1)} (R-\bar\rho z/R)^{m_{\rho ,f}}\) is differentiableAt \(z\) for all \(z\in \overline{{\mathbb D}}_{R}\).

LaTeX Lean

Lemma 274Blaschke nonzero

Let \(0{\lt}R_1{\lt}R{\lt}1\) and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). Then \(\prod _{\rho \in \mathcal K_f(R_1)} (R-\bar\rho z/R)^{m_{\rho ,f}}\neq 0\) for all \(z\in \overline{{\mathbb D}}_{R_1}\setminus \mathcal K_f(R_1)\).

LaTeX Lean

Lemma 353Fraction nonzero

Let \(0{\lt}R{\lt}1\), \(R_1=\frac{2}{3}R\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). Then for any \(\rho \in \mathcal{K}_f(R_1)\), the function \(z \mapsto \frac{R-\bar\rho z/R}{z-\rho }\) is never equal to zero, and differentiableAt \(z\) for all \(z\in \overline{{\mathbb D}}_{R_1}\setminus \mathcal K_f(R_1)\).

LaTeX Lean

Lemma 352Numerator nonzero

Let \(0{\lt}R{\lt}1\), \(R_1=\frac{2}{3}R\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{D}_{R_1}\) with \(f(0)=1\). Then for any \(\rho \in \mathcal{K}_f(R_1)\), the function \(z \mapsto R-\bar\rho z/R\) is never equal to zero, and differentiableAt \(z\) for all \(z\in \overline{{\mathbb D}}_1\).

LaTeX Lean

Lemma 354Power nonzero

Let \(0{\lt}R{\lt}1\), \(R_1=\frac{2}{3}R\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). Then for any \(\rho \in \mathcal{K}_f(R_1)\), the function \(z \mapsto (\frac{R-\bar\rho z/R}{z-\rho })^{m_{\rho ,f}}\) is never equal to zero, and differentiableAt \(z\) for all \(z\in \overline{{\mathbb D}}_{R_1}\setminus \mathcal K_f(R_1)\).

LaTeX Lean

Lemma 355Product nonzero

Let \(0{\lt}R{\lt}1\), \(R_1=\frac{2}{3}R\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). Then the function \(z \mapsto \prod _{\rho \in \mathcal K_f(R_1)} (\frac{R-\bar\rho z/R}{z-\rho })^{m_{\rho ,f}}\) is never equal to zero, and differentiableAt \(z\) for all \(z\in \overline{{\mathbb D}}_{R_1}\setminus \mathcal K_f(R_1)\).

LaTeX Lean

Lemma 296Power mod

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)\neq 0\). Then \(\Big|\left(\frac{R-z\bar\rho /R}{z-\rho }\right)^{m_\rho }\Big|=\left|\frac{R-z\bar\rho /R}{z-\rho }\right|^{m_\rho }\).

LaTeX Lean

Lemma 243Accumulation point

Let \(D\subset {\mathbb C}\) be a compact set. If \(Z\subset D\) is an infinite subset, then \(Z\) has an accumulation point \(\rho _0\in D\).

LaTeX Lean

Lemma 214Bound on error term

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_R\) and \(h\in {\mathbb C}\) satisfy \(z+h \in \overline{{\mathbb D}}_R\) and \(z-h \in \overline{{\mathbb D}}_R\). Let

\[ S_{horiz}(z,h) := \sup _{z.\operatorname {Re}- |h.\operatorname {Re}| \le t \le z.\operatorname {Re}+ |h.\operatorname {Re}|} |f(t + i\, z.\operatorname {Im}) - f(z)| \]

\[ S_{vert}(z,h) := \sup _{z.\operatorname {Im}- |h.\operatorname {Im}| \le \tau \le z.\operatorname {Im}+ |h.\operatorname {Im}|} |f((z+h).\operatorname {Re}+ i\tau ) - f(z)|. \]

\[ S(z,h) := \max (S_{horiz}(z,h),S_{vert}(z,h)) \]

Then the error term \(\mathrm{Err}(z,h)\) is bounded by:

\[ |\mathrm{Err}(z,h)| \le |h.\operatorname {Re}| S(z,h) + |h.\operatorname {Im}|S(z,h). \]

LaTeX Lean

Lemma 215Bound on error term ratio

\[ \left|\frac{\mathrm{Err}(z,h)}{h}\right| \le 2S(z,h). \]

LaTeX Lean

Lemma 171Point bound

Let \(M,R{\gt}0\) and \(0{\lt}r'{\lt}R\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(t \in {\mathbb R}\) we have \(|f(r'e^{it})| \le \frac{2r' M}{R-r'}\).

LaTeX Lean

Lemma 172Integrand bound

Let \(M,R{\gt}0\) and \(0{\lt}r{\lt}r'{\lt}R\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(t \in {\mathbb R}\) we have \(\left|\frac{f(r'e^{it}) r'e^{it}}{(r'e^{it}-z)^2}\right| \le \frac{2(r')^2M}{(R-r')(r'-r)^2}\).

LaTeX Lean

Lemma 267C analytic at K

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)\neq 0\). Then for every \(\sigma \in \mathcal{K}_f(R_1)\), the function \(C_f(z)\) is analyticAt \(\sigma \).

LaTeX Lean

Lemma 258C analytic off K

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)\neq 0\). Then \(C_f(z)\) is analyticAt \(z\) for all \(z \in \overline{{\mathbb D}}_R \setminus \mathcal{K}_f(R_1)\).

LaTeX Lean

Lemma 265C local form

\[ C_f(z) = \frac{h_\sigma (z)}{\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}}}. \]

LaTeX Lean

Lemma 264C off K

\[ C_f(z) = \frac{h_\sigma (z)}{\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}}}. \]

LaTeX Lean

Lemma 261C near zero

\[ C_f(z) = \frac{(z-\sigma )^{m_{\sigma ,f}} h_\sigma (z)}{\prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}}}. \]

LaTeX Lean

Lemma 259C at zero

\[ C_f(z) = \frac{h_\sigma (z)}{\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}}}. \]

LaTeX Lean

Lemma 268C is analytic

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)\neq 0\). Then \(C_f(z)\) is analyticAt \(z\) for all \(z \in \overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 272C never zero

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)\neq 0\). Then \(C_f(z)\neq 0\) for all \(z\in \overline{{\mathbb D}}_{R_1}\).

LaTeX Lean

Lemma 270C nonzero off K

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)\neq 0\). Then \(C_f(z)\neq 0\) for all \(z \in \overline{{\mathbb D}}_{R_1} \setminus \mathcal{K}_f(R_1)\).

LaTeX Lean

Lemma 271C nonzero on K

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)\neq 0\). Then \(C_f(\sigma )\neq 0\) for all \(\sigma \in \mathcal{K}_f(R_1)\).

LaTeX Lean

Lemma 183Denominator form

Given \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \((R-r')(r'-r)^2 = \frac{(R-r)^3}{8}\).

LaTeX Lean

Lemma 184Numerator form

Given \(M{\gt}0\) and \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(2(r')^2M = \frac{(R+r)^2 M}{2}\).

LaTeX Lean

Lemma 181Radius formula

Given \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(R-r' = \frac{R-r}{2}\).

LaTeX Lean

Lemma 182Radius formula

Given \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(r'-r = \frac{R-r}{2}\).

LaTeX Lean

Lemma 41Square expand

For any \(a,c \in {\mathbb R}\), we have \((c-a)^2 = a^2-2ac+c^2\).

LaTeX Lean

Lemma 42Square diff

For any \(a,c \in {\mathbb R}\), we have \((c-a)^2 - a^2 = 2c(c-a)\).

LaTeX Lean

Lemma 206Horizontal strip

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_R\), \(h\in {\mathbb C}\) satisfy \(z+h \in \overline{{\mathbb D}}_R\), and let \(w = (z+h).\operatorname {Re}+ i\, z.\operatorname {Im}\). Then

\[ \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t) dt - \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t + i\, z.\operatorname {Im}) dt + i \int _{0}^{z.\operatorname {Im}} f(w.\operatorname {Re}+ i\tau ) d\tau - i \int _{0}^{z.\operatorname {Im}} f(z.\operatorname {Re}+ i\tau ) d\tau = 0. \]

LaTeX Lean

Lemma 199Cauchy rectangles

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Then for any \(z, w \in \overline{{\mathbb D}}_{R}\),

\begin{align*} \left(\int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(x + i\, z.\operatorname {Im}) \, dx\right) & - \left(\int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(x + i\, w.\operatorname {Im}) \, dx\right) \\ & + i \left(\int _{z.\operatorname {Im}}^{w.\operatorname {Im}} f(w.\operatorname {Re}+ i y) \, dy\right) - i \left(\int _{z.\operatorname {Im}}^{w.\operatorname {Im}} f(z.\operatorname {Re}+ i y) \, dy\right) = 0. \end{align*}

LaTeX Lean

Lemma 134Cauchy’s Integral Formula for \(f'\)

Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\) and any \(r'\) with \(0 {\lt} r {\lt} r' {\lt} R\),

\[ f'(z) = \frac{1}{2\pi i} \oint _{|w|=r'} \frac{f(w)}{(w-z)^2}dw. \]

LaTeX Lean

Lemma 207Rearrangement step

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_R\), \(h\in {\mathbb C}\) satisfy \(z+h \in \overline{{\mathbb D}}_R\), and let \(w = (z+h).\operatorname {Re}+ i\, z.\operatorname {Im}\). Then

\[ i \int _0^{z.\operatorname {Im}} [f(w.\operatorname {Re}+ i\tau ) - f(z.\operatorname {Re}+ i\tau )]\, d\tau = \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t + i\, z.\operatorname {Im})\, dt - \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t)\, dt. \]

LaTeX Lean

Lemma 136CIF for \(f'\), Parameterized

Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\) and any \(r'\) with \(0 {\lt} r {\lt} r' {\lt} R\),

\[ f'(z) = \frac{1}{2\pi i} \int _{0}^{2\pi } \frac{f(r'e^{it})}{(r'e^{it}-z)^2} (ir'e^{it})\, dt. \]

LaTeX Lean

Lemma 137CIF for \(f'\), Simplified

Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\) and any \(r'\) with \(0 {\lt} r {\lt} r' {\lt} R\),

\[ f'(z) = \frac{1}{2\pi } \int _{0}^{2\pi } \frac{f(r'e^{it}) r'e^{it}}{(r'e^{it}-z)^2}\, dt. \]

LaTeX Lean

Lemma 95Boundary modulus

For \(R{\gt}0\), if \(w\in \overline{{\mathbb D}}_R\) and \(w\notin {\mathbb D}_R\), then \(|w|=R\).

LaTeX Lean

Lemma 319Combine bounds

Let \(B{\gt}1\), \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). If \(|B_f(0)|\le B\) then \((3/2)^{\sum _{\rho \in \mathcal K_f(R_1)} m_\rho } \le B\).

LaTeX Lean

Lemma 407Nonzero term

For \(p\in \mathcal{P}\), we have \(1 - p^{-(3/2+it)}\neq 0\).

LaTeX Lean

Lemma 249Finite zeros

Let \(0{\lt}R{\lt}1\) and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be analytic. If there exists \(z\in {\mathbb D}_1\) such that \(f(z)\neq 0\), then \(\mathcal{K}_f(R)\) is finite.

LaTeX Lean

Lemma 20Trig identity

For any \(\theta \in {\mathbb R}\) we have \(2(1+\cos (\theta ))^2 = 3+4\cos (\theta )+\cos (2\theta )\).

LaTeX Lean

Lemma 17Double angle

For any \(\theta \in {\mathbb R}\) we have \(\cos (2\theta ) = 2\cos (\theta )^2 - 1\).

LaTeX Lean

Lemma 18Cos square

For any \(\theta \in {\mathbb R}\) we have \(2\cos (\theta )^2 = 1+\cos (2\theta )\).

LaTeX Lean

Lemma 11Cos even

For \(a\in {\mathbb R}\) we have \(\cos (-a) = \cos (a)\)

LaTeX Lean

Lemma 12Cos even

For \(n\ge 1\), \(y\in {\mathbb R}\) we have \(\cos (-y\log n) = \cos (y\log n)\)

LaTeX Lean

Lemma 19Square expand

For any \(\theta \in {\mathbb R}\) we have \(2(1+\cos (\theta ))^2 = 2 + 4\cos (\theta ) + 2\cos (\theta )^2\).

LaTeX Lean

Lemma 551Zero cos

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

LaTeX Lean

Lemma 466Disk subset

Let \(t\in {\mathbb R}\) with \(|t|{\gt}1\). Let \(c=3/2+it\). Then \(\overline{{\mathbb D}}_1(c) \subset S\)

LaTeX Lean

Lemma 465Disk avoid

Let \(t\in {\mathbb R}\) with \(|t|{\gt}1\). Let \(c=3/2+it\) and \(S_t=\{ s\in {\mathbb C}: s+c\neq 1\} \). Then \(s\neq 1\) for all \(s\in {\mathbb C}\) with \(|s-c|\le 1\).

LaTeX Lean

Lemma 580Log 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)\).

LaTeX Lean

Lemma 581Delta 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)\).

LaTeX Lean

Lemma 203Integral form

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_R\), \(h\in {\mathbb C}\) satisfy \(z+h \in \overline{{\mathbb D}}_R\), and let \(w = (z+h).\operatorname {Re}+ i\, z.\operatorname {Im}\). Then

\[ I_f(w) = \int _0^{(z+h).\operatorname {Re}} f(t)\, dt + i \int _0^{z.\operatorname {Im}} f((z+h).\operatorname {Re}+ i\tau )\, d\tau . \]

LaTeX Lean

Lemma 202Integral form

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_R\). Then

\[ I_f(z) = \int _0^{z.\operatorname {Re}} f(t)\, dt + i \int _0^{z.\operatorname {Im}} f(z.\operatorname {Re}+ i\tau )\, d\tau . \]

LaTeX Lean

Lemma 201Integral form

\[ I_f(z+h) = \int _0^{(z+h).\operatorname {Re}} f(t)\, dt + i \int _0^{(z+h).\operatorname {Im}} f((z+h).\operatorname {Re}+ i\tau )\, d\tau . \]

LaTeX Lean

Lemma 570Delta 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\).

LaTeX Lean

Lemma 582Delta 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\)

LaTeX Lean

Lemma 254Denominator analytic

Let \(S \subset {\mathbb C}\) be a finite set, and for each \(s \in S\), let \(n_s \in \mathbb {N}\) be a positive integer. Then for all \(w\notin S\), the function \(P(z) = \prod _{s \in S} (z-s)^{n_s}\) is analyticAt \(w\) and \(P(w)\neq 0\).

LaTeX Lean

Lemma 113Denom nonzero

Let \(R,M{\gt}0\). Suppose \(f(z)\) is an analytic function on \(|z|\le R\) satisfying \(\Re (f(z)) \le M\). Then \(2M - f(z) \neq 0\) for all \(|z|\le R\).

LaTeX Lean

Lemma 208Shift integral

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_R\), \(h\in {\mathbb C}\) satisfy \(z+h \in \overline{{\mathbb D}}_R\), and let \(w = (z+h).\operatorname {Re}+ i\, z.\operatorname {Im}\). Then

\[ I_f(w) - I_f(z) = \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} f(t + i\, z.\operatorname {Im})\, dt. \]

LaTeX Lean

Lemma 205Initial form

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_R\), \(h\in {\mathbb C}\) satisfy \(z+h \in \overline{{\mathbb D}}_R\), and let \(w = (z+h).\operatorname {Re}+ i\, z.\operatorname {Im}\). Then

\[ I_f(w) - I_f(z) = \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t)\, dt + i \int _0^{z.\operatorname {Im}} [f(w.\operatorname {Re}+ i\tau ) - f(z.\operatorname {Re}+ i\tau )]\, d\tau . \]

LaTeX Lean

Lemma 204Difference form

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_R\), \(h\in {\mathbb C}\) satisfy \(z+h \in \overline{{\mathbb D}}_R\), and let \(w = (z+h).\operatorname {Re}+ i\, z.\operatorname {Im}\). Then

\[ I_f(z+h) - I_f(w) = i \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} f((z+h).\operatorname {Re}+ i\tau )\, d\tau . \]

LaTeX Lean

Lemma 399Diff squares

For any \(z\in {\mathbb C}\), we have \((1-z^2) = (1-z)(1+z)\).

LaTeX Lean

Lemma 463At gives anal

Let open \(T\subset {\mathbb C}\). For \(g:T\to {\mathbb C}\), if \(g\) DifferentiableAt \(s\) for all \(s\in T\), then \(g\) analyticOnNhd \(T\).

LaTeX Lean

Lemma 461At to on

Let \(T\subset {\mathbb C}\). For \(g:T\to {\mathbb C}\), if \(g\) DifferentiableAt \(s\) for all \(s\in T\), then \(g\) DifferentiableOn \(T\)

LaTeX Lean

Lemma 459At to within

Let \(T\subset {\mathbb C}\). For \(g:T\to {\mathbb C}\) and \(s\in T\), if \(g\) DifferentiableAt \(s\) then \(g\) DifferentiableWithinAt \(s\)

LaTeX Lean

Lemma 40Mod diff

For any \(a,b,c \in {\mathbb R}\), we have \(|c-a - ib|^2 - |a + ib|^2 = (c-a)^2 - a^2\).

LaTeX Lean

Lemma 43Mod diff

For any \(a,b,c \in {\mathbb R}\), we have \(|c-a - ib|^2 - |a + ib|^2 = 2c(c-a)\).

LaTeX Lean

Lemma 462Diff to anal

Let open \(T\subset {\mathbb C}\). For \(g:T\to {\mathbb C}\), if \(g\) DifferentiableOn \(T\), then \(g\) analyticOnNhd \(T\)

LaTeX Lean

Lemma 460Within to on

Let \(T\subset {\mathbb C}\). For \(g:T\to {\mathbb C}\), if \(g\) DifferentiableWithinAt \(s\) for all \(s\in T\), then \(g\) DifferentiableOn \(T\)

LaTeX Lean

Lemma 578Imag 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\).

LaTeX Lean

Lemma 577Imag 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\).

LaTeX Lean

Lemma 442Divide split

For any complex number \(z \neq 1\), we have \(\frac{z}{z-1} = 1 + \frac{1}{z-1}\).

LaTeX Lean

Lemma 579Log 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)\).

LaTeX Lean

Lemma 475Disk minus K

Let \(r_1{\gt}0\), \(c\in {\mathbb C}\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1(c)\) with \(f(c)\neq 0\). Let \(f_c(z) = f(z+c)/f(c)\). We have \(z\in \overline{{\mathbb D}}_{r_1} \setminus \mathcal K_{f_c}(R_1)\) if and only if \(z+c\in \overline{{\mathbb D}}_{r_1}(c) \setminus \mathcal K_{f}(R_1;c)\)

LaTeX Lean

Lemma 85Disk split

Let \(T=\{ z\in \ \overline{{\mathbb D}}_R : z\neq 0\} \). Then \(\overline{{\mathbb D}}_R = \{ 0\} \cup T\).

LaTeX Lean

Lemma 99Compactness

For \(R{\gt}0\) the ball \(\overline{{\mathbb D}}_R\) is a compact subset of \({\mathbb C}\).

LaTeX Lean

Lemma 600Real 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)\)

LaTeX Lean

Lemma 239Disk inclusion

Let \(0{\lt}R{\lt}1\). Then we have \(\overline{{\mathbb D}}_R \subset {\mathbb D}_1\).

LaTeX Lean

Lemma 135Differential of \(w(t)\)

For \(w(t) = r'e^{it}\), we have \(dw = ir'e^{it}dt\).

LaTeX Lean

Lemma 145Exp zero one

We have \(e^0 = 1\).

LaTeX Lean

Lemma 14Real cosine

For \(n\ge 1\) and \(y\in {\mathbb R}\) we have \(\Re (e^{-iy\log n}) = \cos (-y\log n)\).

LaTeX Lean

Lemma 15Real cosine

For \(n\ge 1\) and \(y\in {\mathbb R}\) we have \(\Re (n^{-iy}) = \cos (-y\log n)\).

LaTeX Lean

Lemma 16Real cosine

For \(n\ge 1\) and \(y\in {\mathbb R}\) we have \(\Re (n^{-iy}) = \cos (y\log n)\).

LaTeX Lean

Lemma 111Easy maximum principle

Let \(R{\gt}0\) and \(B\ge 0\). Let \(h(z)\) be a function analytic on \(|z| \le R\). Suppose that \(|h(w)| \le B\) for all \(w\in {\mathbb C}\) with \(|w|\le R\). Then \(|h(z)| \le B\) for all \(z\in {\mathbb C}\) with \(|z|= R\).

LaTeX Lean

Lemma 146Cosine relation

For \(t\in {\mathbb R}\) we have \(e^{\Re (it)} = 1\)

LaTeX Lean

Lemma 144Euler part

For \(t\in {\mathbb R}\) we have \(e^{\Re (it)} =e^0\).

LaTeX Lean

Lemma 8Euler’s formula

For \(a\in {\mathbb R}\) we have \(e^{ia} = \cos (a) + i\sin (a)\)

LaTeX Lean

Lemma 427Main integral

For \(s\in {\mathbb C}, s\neq 1\), we have \(s \int _1^N u^{-s} du = \frac{s}{1-s}(N^{1-s} - 1)\).

LaTeX Lean

Lemma 222Exponential of \(I_f\) at zero

LaTeX Lean

Lemma 227Derivative of \(\exp (J(z))\)

\[ (\exp (J(z)))' = J'(z) \cdot \exp (J(z)). \]

LaTeX Lean

Lemma 494Sum 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). \]

LaTeX Lean

Lemma 495Real 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). \]

LaTeX

Lemma 496Split 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). \]

LaTeX Lean

Lemma 497Double 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). \]

LaTeX Lean

Lemma 511Double 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). \]

LaTeX Lean

Lemma 10Log inverse

For \(n\ge 1\) we have \(n = e^{\log n}\).

LaTeX Lean

Lemma 5Exp rule

For any \(n\ge 1\) and \(\alpha ,\beta \in {\mathbb C}\) we have \(n^{\alpha +\beta } = n^\alpha \cdot n^{\beta }\)

LaTeX Lean

Lemma 100ExtrValThm

If \(K\subset {\mathbb C}\) is compact and \(g:K \to {\mathbb C}\) is continuous, then there exists \(v\in K\) such that \(|g(v)| \ge |g(z)|\) for all \(z\in K\).

LaTeX Lean

Lemma 101Disk Boundary

If \(g:\overline{{\mathbb D}}_R \to {\mathbb C}\) is continuous, then there exists \(v\in \overline{{\mathbb D}}_R\) such that \(|g(v)| \ge |g(z)|\) for all \(z\in \overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 103Max modulus

If \(h:\overline{{\mathbb D}}_R \to {\mathbb C}\) is analytic, then there exists \(u\in \overline{{\mathbb D}}_R\) such that \(|h(u)| \ge |h(z)|\) for all \(z\in \overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 129Rearranged bound

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(0{\lt}r {\lt} R\) and any \(z\in {\mathbb C}\) with \(|z|=r\), we have \(R|f(z)| \le r|2M - f(z)|\).

LaTeX Lean

Lemma 356Outside zeros

Let \(0{\lt}R{\lt}1\), \(R_1=\frac{2}{3}R\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). Then the function \(f(z)\) is never equal to zero, and differentiableAt \(z\) for all \(z\in \overline{{\mathbb D}}_{R_1}\setminus \mathcal K_f(R_1)\).

LaTeX Lean

Lemma 282Not zero

Let \(f:{\mathbb C}\to {\mathbb C}\). If \(f(0)\neq 0\), then \(f\) is not the identically zero function.

LaTeX Lean

Lemma 269f nonzero off K

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)\neq 0\). Then \(f(z)\neq 0\) for all \(z \in \overline{{\mathbb D}}_{R_1} \setminus \mathcal{K}_f(R_1)\).

LaTeX Lean

Lemma 177Derivative bound

Let \(M,R{\gt}0\) and \(0{\lt}r{\lt}r'{\lt}R\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). Then we have \(|f'(z)| \le \frac{2(r')^2M}{(R-r')(r'-r)^2}\).

LaTeX Lean

Lemma 174Derivative bound

Let \(M,R{\gt}0\) and \(0{\lt}r{\lt}r'{\lt}R\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(t \in {\mathbb R}\) we have \(|f'(z)| \le \frac{1}{2\pi } \int _{0}^{2\pi } \frac{2(r')^2M}{(R-r')(r'-r)^2} dt\).

LaTeX Lean

Lemma 114Ratio bound

Let \(R,M{\gt}0\). Suppose \(f(z)\) is an analytic function on \(|z|\le R\) satisfying \(\Re (f(z)) \le M\). For any \(z\) with \(|z| \le R\), we have \( \frac{|f(z)|}{|2M - f(z)|}\le 1\).

LaTeX Lean

Lemma 123Scaled ratio

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(z\) with \(|z| \le R\), we have \( \frac{|f(z)|/R}{|2M - f(z)|}\le 1/R\).

LaTeX Lean

Lemma 470Normalize analytic

Let \(c\in {\mathbb C}\) and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1(c)\) with \(f(c)\neq 0\). Then the function \(f_c(z) = f(z+c)/f(c)\) is AnalyticOnNhd \(\overline{{\mathbb D}}_1\) and satisfies \(f_c(0)=1\).

LaTeX Lean

Lemma 472Shift bound

Let \(B{\gt}1\), \(0{\lt}R{\lt}1\), \(c\in {\mathbb C}\), and \(f:{\mathbb C}\to {\mathbb C}\) with \(f(c)\neq 0\). If \(|f(z)|\le B\) for all \(z\in \overline{{\mathbb D}}_R(c)\), then the function \(f_c(z) = f(z+c)/f(c)\) satisfies \(|f_c(z)| \le B/|f(c)|\) for all \(z\overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 471Log derivative

Let \(c\in {\mathbb C}\) and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1(c)\) with \(f(c)\neq 0\). Let \(f_c(z) = f(z+c)/f(c)\). Then for any \(z\) where \(f(z+c) \neq 0\), we have \(\text{logDeriv}(f_c)(z) = \text{logDeriv}(f)(z+c)\).

LaTeX Lean

Lemma 474Order shift

Let \(r{\gt}0\), \(c\in {\mathbb C}\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1(c)\) with \(f(c)\neq 0\). Let \(f_c(z) = f(z+c)/f(c)\). For \(\rho \in \mathcal{K}_{f_c}(r)\), the analyticOrderAt satisfies \(m_{\rho ,f_c} = m_{\rho +c,f}\).

LaTeX Lean

Lemma 473Zero shift

Let \(r{\gt}0\), \(c\in {\mathbb C}\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1(c)\) with \(f(c)\neq 0\). Let \(f_c(z) = f(z+c)/f(c)\). We have \(\rho '\in \mathcal{K}_{f_c}(r)\) if and only if \(\rho '=\rho -c\) where \(\rho \in \mathcal{K}_f(r;c)\). In particular \(\mathcal{K}_{f_c}(r) = \{ \rho -c : \rho \in \mathcal{K}_f(r) \} \).

LaTeX Lean

Lemma 420Power deriv

Let \(f(u) = u^{-s}\). Then \(f'(u) = -s u^{-s-1}\).

LaTeX Lean

Lemma 131Circle bound

\[ |f(z)| \le \frac{2r}{R-r}M. \]

LaTeX Lean

Lemma 130Circle bound

\[ |f(z)| \le \frac{2r}{R-r}M. \]

LaTeX Lean

Lemma 383Final bound

Let \(B{\gt}1\), \(0{\lt}r_1{\lt}r{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). If \(|f(z)|\le B\) on \(|z|\le R\), then for all \(z\in \overline{{\mathbb D}}_{r_1}\setminus \mathcal K_f(R_1)\) we have

\[ \left|\frac{f'}{f}(z) - \sum _{\rho \in \mathcal K_f(R_1)}\frac{m_{\rho ,f}}{z-\rho }\right| \le \left(\frac{16 r^2}{(r-r_1)^3} + \frac{1}{(R^2/R_1 - R_1)\log (R/R_1)}\right)\log B. \]

LaTeX Lean

Lemma 476Final bound

Let \(B{\gt}1\), \(0{\lt}r_1{\lt}r{\lt}R_1{\lt}R{\lt}1\). Let \(c\in {\mathbb C}\) and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1(c)\) with \(f(c)\neq 0\). Let \(f_c(z) = f(z+c)/f(c)\). If \(|f(z)| {\lt} B\) for all \(z\in \overline{{\mathbb D}}_R(c)\), then for all \(z\in \overline{{\mathbb D}}_{r_1} \setminus \mathcal K_{f_c}(R_1)\) we have

\[ \left|\frac{f_c'}{f_c}(z) - \sum _{\rho '\in \mathcal K_{f_c}(R_1)}\frac{m_{\rho ',f_c}}{z-\rho '}\right| \le \left(\frac{16 r^2}{(r-r_1)^3} + \frac{1}{(R^2/R_1 - R_1)\log (R/R_1)}\right)\log (B/|f(c)|). \]

LaTeX Lean

Lemma 382Final bound

\[ \left|\frac{f'}{f}(z) - \sum _{\rho \in \mathcal K_f(R_1)}\frac{m_{\rho ,f}}{z-\rho }\right| \le \frac{16\log (B) r^2}{(r-r_1)^3} + \frac{\log B}{(R^2/R_1 - R_1)\log (R/R_1)}. \]

LaTeX Lean

Lemma 381Final sum

Let \(B{\gt}1\), \(0{\lt}R_1{\lt} R{\lt}1\) and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). If \(|f(z)|\le B\) on \(|z|\le R\), then for all \(z\in \overline{{\mathbb D}}_{R_1}\setminus \mathcal K_f(R_1)\) we have

\[ \left|\sum _{\rho \in \mathcal K_f(R_1)}\frac{m_{\rho ,f}}{z-R^2/\bar\rho }\right| \le \frac{\log B}{(R^2/R_1 - R_1) \log (R/R_1)}. \]

LaTeX Lean

Lemma 453Algebra step

For \(|t|\ge 1\), we have \(1 + 1 + (3+|t|) \cdot 2 = 8 + 2|t|\).

LaTeX Lean

Lemma 452Combine bounds

If \(s=\sigma +it\) with \(\tfrac {1}{2} \le \sigma {\lt} 3\) and \(|t|\ge 1\), then

\[ |\zeta (s)| {\lt} 1 + 1 + (3+|t|) \cdot 2. \]

LaTeX Lean

Lemma 589Finite set

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

LaTeX Lean

Lemma 422Floor int

For an integer \(N\ge 1\), \(\lfloor N \rfloor = N\).

LaTeX Lean

Lemma 424Floor split

For any \(u\in {\mathbb R}\), \(\lfloor u \rfloor = u - \{ u\} \), where \(\{ u\} \) is the fractional part of \(u\).

LaTeX Lean

Lemma 185Fraction simplify

Given \(M{\gt}0\) and \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(\frac{2(r')^2M}{(R-r')(r'-r)^2} = \frac{(R+r)^2 M/2}{(R-r)^3/8}\).

LaTeX Lean

Lemma 186Fraction simplify

Given \(M{\gt}0\) and \(0 {\lt} r {\lt} R\), we have \(\frac{(R+r)^2 M/2}{(R-r)^3/8} = \frac{4(R+r)^2 M}{(R-r)^3}\).

LaTeX Lean

Lemma 187Fraction simplify

Given \(M{\gt}0\) and \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(\frac{2(r')^2M}{(R-r')(r'-r)^2} = \frac{4(R+r)^2 M}{(R-r)^3}\).

LaTeX Lean

Lemma 197Fraction simplify

Given \(M{\gt}0\) and \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(\frac{2(r')^2M}{(R-r')(r'-r)^2} \leq \frac{16R^2 M}{(R-r)^3}\).

LaTeX Lean

Lemma 430Frac bound

For any \(u\in {\mathbb R}\), \(0 \le \{ u\} {\lt} 1\), and thus \(|\{ u\} | \le 1\).

LaTeX Lean

Lemma 128Fraction swap

Let \(a,b,r,R{\gt}0\). If \(\frac{a/r}{b} \le 1/R\) then \(Ra \le rb\).

LaTeX Lean

Lemma 280Zero value

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\). If \(\rho \in \mathcal K_f(R_1)\) then \(f(\rho )=0\).

LaTeX Lean

Lemma 281Zero contrapositive

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\). If \(f(\rho )\neq 0\) then \(\rho \notin \mathcal K_f(R_1)\).

LaTeX Lean

Lemma 121Quotient radius

Let \(T{\gt}0\) and \(z,w\in {\mathbb C}\). If \(|z|=T\) then \(|w/z| = |w|/T\).

LaTeX Lean

Lemma 82Quotient analytic

Let \(T=\{ z\in \ \overline{{\mathbb D}}_R : z\neq 0\} \) and \(f:{\mathbb C}\to {\mathbb C}\). If \(f(z)\) is analytic on \(\overline{{\mathbb D}}_R\), then \(f(z)/z\) is analytic on \(T\).

LaTeX Lean

Lemma 118g analytic

The function \(f_M(z)\) from Definition 117 is analytic on \(|z| \le R\).

LaTeX Lean

Lemma 126g at r

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(0{\lt}r{\lt}R\) and any \(z\in {\mathbb C}\) with \(|z|=r\), we have \(|f_M(z)| = \frac{|f(z)|/r}{|2M - f(z)|}\).

LaTeX Lean

Lemma 127g bound r

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(0{\lt}r{\lt}R\) and any \(z\in {\mathbb C}\) with \(|z|=r\), we have \(\frac{|f(z)|/r}{|2M - f(z)|} \le 1/R\).

LaTeX Lean

Lemma 124Boundary bound

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(z\in {\mathbb C}\) with \(|z|=R\), we have \(|f_M(z)| \le 1/R\).

LaTeX Lean

Lemma 125Interior bound

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(z\in {\mathbb C}\) with \(|z| \le R\), we have \(|f_M(z)| \le 1/R\).

LaTeX Lean

Lemma 122Boundary g

LaTeX Lean

Lemma 120g modulus

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). We have \(|f_M(z)| = \frac{|f(z)/z|}{|2M - f(z)|}\).

LaTeX Lean

Lemma 223Value of \(H\) at zero

Let \(0{\lt}R{\lt}R_0{\lt}1\), assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Let \(H\) be the function from definition 221. Then \(H(0)=1/B(0)\).

LaTeX Lean

Lemma 228Derivative of \(H(z)\)

Let \(0{\lt}R{\lt}R_0{\lt}1\), assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Let \(J\) and \(H\) be the functions from definition 221. The derivative of \(H(z)\) is given by

\[ H'(z) = \frac{\big(J'(z) B(z) - B'(z)\big)\exp (J(z))}{B(z)^2}. \]

LaTeX Lean

Lemma 229Derivative of \(H(z)\) is 0

Let \(0{\lt}R{\lt}R_0{\lt}1\), assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Let \(J\) and \(H\) be the functions from definition 221. Then \(H'(z) = 0\) for all \(z \in \overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 226Derivative of \(H(z)\)

Let \(0{\lt}R{\lt}R_0{\lt}1\), assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Let \(J\) and \(H\) be the functions from definition 221. The derivative of \(H(z)\) is given by

\[ H'(z) = \frac{(\exp (J(z)))' \cdot B(z) - B'(z) \cdot \exp (J(z))}{B(z)^2}. \]

LaTeX Lean

Lemma 230\(H(z)\) is constant

Let \(0{\lt}R{\lt}R_0{\lt}1\), assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Let \(H\) be from definition 221. Then \(H(z)=H(0)\) for all \(z\in \overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 231\(H=1\)

Let \(0{\lt}R{\lt}R_0{\lt}1\), assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\), \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Let \(H\) be the function from definition 221. Then \(H(z)=1/B(0)\) for all \(z \in \overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 266h ratio analytic

Let \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)\neq 0\). For each \(\sigma \in \mathcal{K}_f(R_1)\), the function \(\frac{h_\sigma (z)}{\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}}}\) is analyticAt \(\sigma \).

LaTeX Lean

Lemma 110Max principle

Let \(R{\gt}0\) and \(B\ge 0\). Let \(h(z)\) be a function analytic on \(|z| \le R\). Suppose that \(|h(z)| \le B\) for all \(z\in {\mathbb C}\) with \(|z|= R\). Then \(|h(w)| \le B\) for all \(w\in {\mathbb C}\) with \(|w|\le R\).

LaTeX Lean

Lemma 220Antiderivative of logarithmic derivative

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Then there exists \(J: \overline{{\mathbb D}}_R\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R}\), such that \(J(0)=0\) and \(J'(z) = B'(z)/B(z)\) for all \(z \in \overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 248Infinite zeros imply

Let \(0{\lt}R{\lt}1\) and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be analytic. If \(\mathcal{K}_f(R)\) is infinite, then \(f(z)=0\) for all \(z\in {\mathbb D}_1\).

LaTeX Lean

Lemma 245Identity theorem

Let \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be analytic. Suppose there exists \(\rho _0\in {\mathbb D}_1\) an accumulation point of \(\{ \rho \in {\mathbb D}_1 : f(\rho )=0\} \). Then \(f(z)=0\) for all \(z\in {\mathbb D}_1\).

LaTeX Lean

Lemma 247Identity on K

Let \(0{\lt}R{\lt}1\) and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be analytic. Suppose there exists \(\rho _0\in \overline{{\mathbb D}}_R\) an accumulation point of \(\mathcal{K}_f(R)\). Then \(f(z)=0\) for all \(z\in {\mathbb D}_1\).

LaTeX Lean

Lemma 246Identity theorem R

Let \(0{\lt}R{\lt}1\) and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be analytic. Suppose there exists \(\rho _0\in \overline{{\mathbb D}}_R\) an accumulation point of \(\{ \rho \in {\mathbb D}_1 : f(\rho )=0\} \). Then \(f(z)=0\) for all \(z\in {\mathbb D}_1\).

LaTeX Lean

Lemma 210Add-sub step

\[ I_f(z+h)-I_f(z) = \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} (f(t + i\, z.\operatorname {Im}) - f(z) + f(z))\, dt + i \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} (f((z+h).\operatorname {Re}+ i\tau ) - f(z) + f(z))\, d\tau . \]

LaTeX Lean

Lemma 213Difference decomposition

\[ I_f(z+h)-I_f(z) = h \cdot f(z) + \mathrm{Err}(z,h), \]

where \(\mathrm{Err}(z,h)\) is defined as

\[ \mathrm{Err}(z,h) := \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} (f(t + i\, z.\operatorname {Im}) - f(z))\, dt + i \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} (f((z+h).\operatorname {Re}+ i\tau ) - f(z))\, d\tau . \]

LaTeX Lean

Lemma 211Linearity split

\begin{align*} I_f(z+h)-I_f(z) = & \left( \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} (f(t + i\, z.\operatorname {Im}) - f(z))\, dt + \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} f(z)\, dt \right) \\ & + i \left( \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} (f((z+h).\operatorname {Re}+ i\tau ) - f(z))\, d\tau + \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} f(z)\, d\tau \right). \end{align*}

LaTeX Lean

Lemma 209L path

\[ I_f(z+h)-I_f(z) = \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} f(t + i\, z.\operatorname {Im})\, dt + i \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} f((z+h).\operatorname {Re}+ i\tau )\, d\tau . \]

LaTeX Lean

Lemma 218Differentiability of \(I_f(z)\)

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). The function \(I_f(z)\) is analyticOnNhd \(\overline{{\mathbb D}}_{R}\), and \(I'_f(z)=f(z)\) on \(\overline{{\mathbb D}}_{R}\).

LaTeX Lean

Lemma 92In disk bound

For \(R{\gt}0\), if \(w\in \overline{{\mathbb D}}_R\) then \(|w|\le R\).

LaTeX Lean

Lemma 188Inequality fact

Given \(r {\lt} R\), we have \(R+r {\lt} 2R\).

LaTeX Lean

Lemma 194Square bound

Given \(0 {\lt} r {\lt} R\), we have \((R+r)^2 {\lt} 4R^2\).

LaTeX Lean

Lemma 192Square bound

Given e, we have \((R+r)^2 {\lt} (2R)^2\).

LaTeX Lean

Lemma 195Square bound

Given \(M{\gt}0\) and \(0 {\lt} r {\lt} R\), we have \(4(R+r)^2M {\lt} 16R^2M\).

LaTeX Lean

Lemma 52Divide inequality

If \(c{\gt}0\) and \(0\le a\le b\), then \(a/c\le b/c\).

LaTeX Lean

Lemma 53Ratio bound

If \(b{\gt}0\) and \(0\le a\le b\), then \(a/b\le 1\).

LaTeX Lean

Lemma 29Inequality reversal

For \(x, M\in {\mathbb R}\), if \(x \le M\) then \(2M-x \ge M\).

LaTeX Lean

Lemma 173Integral inequality

If \(g(t) \le C\) for all \(t \in [a,b]\), then \(\int _a^b g(t) dt \le \int _a^b C dt\).

LaTeX Lean

Lemma 176Exponential integral

We have \(\frac{1}{2\pi }\int _0^{2\pi } dt = 1\).

LaTeX Lean

Lemma 139Integral bound

For an integrable function \(g(t)\), we have \(|\int _a^b g(t) dt| \le \int _a^b |g(t)| dt\).

LaTeX Lean

Lemma 175Integrate one

We have \(\int _0^{2\pi } dt = 2\pi \).

LaTeX Lean

Lemma 212Integral of constant over L-path

\[ \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} f(z)\, dt + i \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} f(z)\, d\tau = f(z) \cdot h. \]

LaTeX Lean

Lemma 440Integral analytic

If the integral of an analytic function \(f:{\mathbb C}\to {\mathbb C}\) converges uniformly for all \(s\) such that \(\Re (s) \ge \frac{1}{10}\), then the integral is analytic (as a function of s).

LaTeX Lean

Lemma 445Integral value

For \(\Re (s){\gt}0\), \(\int _1^\infty u^{-\Re (s)-1} du = \frac{1}{\Re (s)}\).

LaTeX Lean

Lemma 434Integral conv

Let \(\varepsilon {\gt}0\) If \(\Re (s)\ge \varepsilon \), the integral \(\int _1^\infty \{ u\} u^{-s-1} du\) converges uniformly.

LaTeX Lean

Lemma 425Integral split

For \(s\in {\mathbb C}\) and integer \(N\ge 1\),

\[ \int _1^N \lfloor u \rfloor u^{-s-1} du = \int _1^N u^{-s} du - \int _1^N \{ u\} u^{-s-1} du. \]

LaTeX Lean

Lemma 431Term bound

For \(u\ge 1\) and \(s\in {\mathbb C}\), \(|\{ u\} u^{-s-1}| \le u^{-\Re (s)-1}\).

LaTeX Lean

Lemma 432Eps bound

Let \(\varepsilon {\gt}0\) and \(u\ge 1\). If \(\Re (s)\ge \varepsilon \) then \(|\{ u\} u^{-s-1}| \le u^{-1-\varepsilon }\).

LaTeX Lean

Lemma 406Inv order

If \(0 {\lt} a \le b\), then \(a^{-1} \ge b^{-1}\).

LaTeX Lean

Lemma 290Inverse bound

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\) with \(f(0)\neq 0\). If \(\rho \in \mathcal K_f(R_1)\) then \(1/|\rho |\ge 1/R_1\).

LaTeX Lean

Lemma 289Inverse mono

Let \(x, y \in {\mathbb R}\). If \(0 {\lt} x \le y\), then \(1/x \ge 1/y\).

LaTeX Lean

Lemma 450Real inv

If \(\tfrac {1}{2} \le \Re (s) {\lt} 3\), then \(\dfrac {1}{\Re (s)} \le 2\).

LaTeX Lean

Lemma 451Shift bound

Let \(s=\sigma +it\). If \(\tfrac {1}{2} \le \sigma {\lt} 3\) and \(|t|\ge 1\), then \(|s-1| \ge 1\).

LaTeX Lean

Lemma 320Jensen form

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\). If \(f(0)=1\) and \(|f(z)|\le B\) on \(|z|\le R\), then \((3/2)^{\sum _{\rho \in \mathcal K_f(R_1)} m_\rho } \le B\).

LaTeX Lean

Lemma 322Jensen log

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\). If \(f(0)=1\) and \(|f(z)|\le B\) on \(|z|\le R\), then \(\sum _{\rho \in \mathcal K_f(R_1)} m_\rho \log (3/2) \le \log B\).

LaTeX Lean

Lemma 260Zeros isolated

Let \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)\neq 0\). For any \(\sigma ,\rho \in \mathcal{K}_f(R_1)\) with \(\sigma \neq \rho \), Eventually for \(z\) in nbhds of \(\sigma \), we have \(z\neq \rho \).

LaTeX Lean

Lemma 241Zero containment

Let \(R{\gt}0\) and \(f:\overline{{\mathbb D}}_R\to {\mathbb C}\). Then we have \(\mathcal{K}_f(R) \subset \overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 242Zero in disk

Let \(0{\lt}R{\lt}1\) and \(f:{\mathbb D}_1\to {\mathbb C}\). Then we have \(\mathcal{K}_f(R) \subset \{ \rho \in {\mathbb D}_1 : f(\rho )=0 \} \).

LaTeX Lean

Lemma 615Zero 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*}

LaTeX Lean

Lemma 613Empty set

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

LaTeX Lean

Lemma 561Term 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))\).

LaTeX Lean

Lemma 94Modulus equal

For \(R{\gt}0\), if \(|w|\le R\) and \(|w|\ge R\) then \(|w|=R\).

LaTeX Lean

Lemma 335Lf at zero

Let \(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\) with \(f(0)=1\). We have \(L_f(0) = 0\).

LaTeX Lean

Lemma 376Final formula

\[ L'_f(z)=\frac{f'}{f}(z) - \sum _{\rho \in \mathcal K_f(R_1)}\frac{m_{\rho ,f}}{z-\rho } + \sum _{\rho \in \mathcal K_f(R_1)}\frac{m_{\rho ,f}}{z-R^2/\bar\rho }. \]

LaTeX Lean

Lemma 346Derivative form

Let \(0{\lt}R{\lt}1\) and \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). We have \(\text{logDeriv}(B_f(z)/B_f(0))=\text{logDeriv}(B_f(z))\).

LaTeX Lean

Lemma 361Step one

Let \(0{\lt}r{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). Then for all \(z\in \overline{{\mathbb D}}_{r}\setminus \mathcal K_f(R_1)\) we have

\[ L'_f(z)=\frac{f'}{f}(z) + \text{logDeriv}\left(\prod _{\rho \in \mathcal K_f(R_1)}\left(\frac{R-z\bar\rho /R}{z-\rho }\right)^{m_{\rho ,f}}\right) \]

LaTeX Lean

Lemma 365Step two

\[ L'_f(z)=\frac{f'}{f}(z) + \sum _{\rho \in \mathcal K_f(R_1)}m_{\rho ,f} \text{logDeriv}\left(\frac{R-z\bar\rho /R}{z-\rho }\right). \]

LaTeX Lean

Lemma 373Step three

Let \(0{\lt}r{\lt}R_1{\lt}R\), \(R {\lt} 1\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). Then for all \(z\in \overline{{\mathbb D}}_{r}\setminus \mathcal K_f(R_1)\) we have \(L'_f(z)=\frac{f'}{f}(z) + \sum _{\rho \in \mathcal K_f(R_1)}m_{\rho ,f}\left( \frac{1}{z-R^2/\bar\rho } - \frac{1}{z-\rho }\right)\).

LaTeX Lean

Lemma 334Lf analytic

Let \(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\) with \(f(0)=1\). Then \(L_f(z)\) is AnalyticOnNhd \(\overline{{\mathbb D}}_{r}\).

LaTeX Lean

Lemma 217Limit of error term ratio is zero

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_{R}\). Then

\[ \lim _{h\to 0} \frac{\mathrm{Err}(z,h)}{h} = 0. \]

LaTeX Lean

Lemma 216Limit of \(S(z,h)\) is zero

\[ \lim _{h\to 0} S(z,h) = 0. \]

LaTeX Lean

Lemma 429Limit term

If \(\Re (s){\gt}1\), then \(\lim _{N\to \infty } N^{1-s} = 0\).

LaTeX Lean

Lemma 4Log compare

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

LaTeX Lean

Lemma 512Log compare

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

LaTeX Lean

Lemma 514Log compare

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

LaTeX Lean

Lemma 3Double log

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

LaTeX Lean

Lemma 340Log nonnegative

Let \(0{\lt}R_1{\lt}R{\lt}1\) and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). Then \(\log |B_f(0)| \ge 0\).

LaTeX Lean

Lemma 337Log bound

Let \(B{\gt}1\), \(0{\lt}R_1{\lt}R{\lt}1\) and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\). If \(0{\lt}|B_f(z)|\) and \(|B_f(z)|\le B\) for all \(|z|\le R_1\), then \(\log |B_f(z)| \le \log B\) for all \(|z|\le R_1\).

LaTeX Lean

Lemma 338Log bound

Let \(B{\gt}1\), \(0{\lt}R_1{\lt}R{\lt}1\) and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\). If \(|B_f(z)|\le B\) for all \(|z|\le R\), then \(\log |B_f(z)| \le \log B\) for all \(|z|\le R_1\).

LaTeX Lean

Lemma 339Log bound

Let \(B{\gt}1\), \(0{\lt}R_1{\lt}R{\lt}1\) and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\). If \(|f(z)|\le B\) on \(|z|\le R\), then \(\log |B_f(z)| \le \log B\) for all \(|z|\le R_1\).

LaTeX Lean

Lemma 477Log expansion

Let \(t\in {\mathbb R}\) with \(|t|{\gt}3\). Let \(c=3/2+it\), \(B{\gt}1\), \(0{\lt}r_1{\lt}r{\lt}R_1{\lt}R{\lt}1\). If \(|\zeta (z)| {\lt} B\) for all \(z\in \overline{{\mathbb D}}_R(c)\), then for all \(z\in \overline{{\mathbb D}}_{r_1}(c)\setminus \mathcal K_\zeta (R_1;c)\) we have

\begin{align*} \left|\frac{\zeta '(z)}{\zeta (z)} - \sum _{\rho \in \mathcal K_{\zeta }(R_1;c)} \frac{m_{\rho ,\zeta }}{z-\rho } \right| \le \left(\frac{16 r^2}{(r-r_1)^3} + \frac{1}{(R^2/R_1 - R_1)\log (R/R_1)}\right) \log (B/|\zeta (c)|) \end{align*}

LaTeX Lean

Lemma 224Logarithmic derivative identity

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). For \(J\) from lemma 220, then \(J'(z)B(z) = B'(z)\) for all \(z \in \overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 225Logarithmic derivative identity

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). For \(J\) from lemma 220, then \(J'(z)B(z) - B'(z) = 0\) for all \(z \in \overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 219Logarithmic derivative is analytic

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Then the function \(B'(z)/B(z)\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\).

LaTeX Lean

Lemma 236Logarithm of modulus as sum

LaTeX Lean

Lemma 321Log monotone

Let \(x,y \in {\mathbb R}\). If \(0 {\lt} x \le y\), then \(\log x \le \log y\).

LaTeX Lean

Lemma 238Logarithm of an analytic function

Let \(0{\lt}R{\lt}R_0{\lt}1\), assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) with \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Then there exists \(J_B: \overline{{\mathbb D}}_R\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R}\), such that \(J_B(0)=0\), and \(J_B'(z) = B'(z)/B(z)\) and \(\log |B(z)| - \log |B(0)| = \Re (J_B(z))\) for all \(z \in \overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 359Log sum

Let \(0{\lt}R{\lt}1\), \(R_1=\frac{2}{3}R\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). Then for all \(z\in \overline{{\mathbb D}}_{R_1}\setminus \mathcal K_f(R_1)\) we have

\[ \text{logDeriv}(B_f(z))=\text{logDeriv}(f(z)) + \text{logDeriv}\left(\prod _{\rho \in \mathcal K_f(R_1)}\left(\frac{R-z\bar\rho /R}{z-\rho }\right)^{m_{\rho ,f}}\right). \]

LaTeX Lean

Lemma 366Difference form

\[ \text{logDeriv}\left(\frac{R-z\bar\rho /R}{z-\rho }\right) = \text{logDeriv}(R-z\bar\rho /R) - \text{logDeriv}(z-\rho ). \]

LaTeX Lean

Lemma 372Diff fraction

Let \(0{\lt}R{\lt}1\), \(R_1=\frac{2}{3}R\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\). For \(\rho \in \mathcal{K}_f(R_1)\), we have \(\text{logDeriv}\left(\frac{R-z\bar\rho /R}{z-\rho }\right) = \frac{1}{z-R^2/\bar\rho } - \frac{1}{z-\rho }\).

LaTeX Lean

Lemma 360Fraction form

Let \(f\) be a non-zero analytic function. Then \(\text{logDeriv}(f(z)) = \frac{f'}{f}(z)\).

LaTeX Lean

Lemma 368Denominator rule

Let \(\rho \in {\mathbb C}\). We have \(\text{logDeriv}(z-\rho ) = \frac{1}{z-\rho }\) at \(z\neq \rho \).

LaTeX Lean

Lemma 358Log sum

\[ \text{logDeriv}\left(f(z)\prod _{\rho \in \mathcal K_f(R_1)}\left(\frac{R-z\bar\rho /R}{z-\rho }\right)^{m_{\rho ,f}}\right)=\text{logDeriv}(f(z)) + \text{logDeriv}\left(\prod _{\rho \in \mathcal K_f(R_1)}\left(\frac{R-z\bar\rho /R}{z-\rho }\right)^{m_{\rho ,f}}\right). \]

LaTeX Lean

Lemma 367Linear rule

Let \(a,b \in {\mathbb C}\) with \(a\neq 0\). We have \(\text{logDeriv}(az+b) = \frac{a}{az+b}\) at \(z\neq -b/a\).

LaTeX Lean

Lemma 371Numerator form

Let \(R, \rho \in {\mathbb C}\). We have \(\text{logDeriv}(R-z\bar\rho /R) = \frac{1}{z-R^2/\bar\rho }\).

LaTeX Lean

Lemma 369Numerator rule

Let \(R, \rho \in {\mathbb C}\). We have \(\text{logDeriv}(R-z\bar\rho /R) = \frac{-\bar\rho /R}{R-z\bar\rho /R}\).

LaTeX Lean

Lemma 370Rearranged form

Let \(R, \rho \in {\mathbb C}\). We have \(\frac{-\bar\rho /R}{R-z\bar\rho /R} = \frac{1}{z-R^2/\bar\rho }\).

LaTeX Lean

Lemma 363Power multiple

\[ \text{logDeriv}\left(\left(\frac{R-z\bar\rho /R}{z-\rho }\right)^{m_{\rho ,f}}\right) = m_{\rho ,f} \, \text{logDeriv}\left(\frac{R-z\bar\rho /R}{z-\rho }\right). \]

LaTeX Lean

Lemma 362Product sum

\[ \text{logDeriv}\left(\prod _{\rho \in \mathcal K_f(R_1)}\left(\frac{R-z\bar\rho /R}{z-\rho }\right)^{m_{\rho ,f}}\right) = \sum _{\rho \in \mathcal K_f(R_1)}\text{logDeriv}\left(\left(\frac{R-z\bar\rho /R}{z-\rho }\right)^{m_{\rho ,f}}\right) \]

LaTeX Lean

Lemma 364Sum multiple

\[ \text{logDeriv}\left(\prod _{\rho \in \mathcal K_f(R_1)}\left(\frac{R-z\bar\rho /R}{z-\rho }\right)^{m_{\rho ,f}}\right) = \sum _{\rho \in \mathcal K_f(R_1)}m_{\rho ,f} \text{logDeriv}\left(\frac{R-z\bar\rho /R}{z-\rho }\right). \]

LaTeX Lean

Lemma 344Constant rule

Let \(a\in {\mathbb C}\) with \(a\neq 0\) and \(g:\overline{D}_1\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\). Then \(\text{logDeriv}(a\cdot g(z)) = \text{logDeriv}(g(z))\).

LaTeX Lean

Lemma 349Quotient rule

Let \(h,g\) be functions differentiableAt \(z\) with \(h(z),g(z)\neq 0\). Then \(\text{logDeriv}(h/g) = \text{logDeriv}(h)-\text{logDeriv}(g)\) at \(z\).

LaTeX Lean

Lemma 350Power rule

Let \(m\in {\mathbb N}\) and let \(g\) be a function differentiableAt \(z\). Then \(\text{logDeriv}(g(z)^m)=m\cdot \text{logDeriv}(g(z))\).

LaTeX Lean

Lemma 347Product rule

Let \(f,g\) be functions differentiableAt \(z\) with \(f(z),g(z)\neq 0\). Then \(\text{logDeriv}(f\cdot g) = \text{logDeriv}(f)+\text{logDeriv}(g)\) at \(z\).

LaTeX Lean

Lemma 348Product sum

Let \(K\) be a finite set and \(\{ g_\rho (z)\} _{\rho \in K}\) be a collection of functions differentiableAt \(z\) with \(g_\rho (z)\neq 0\) for all \(\rho \in K\). Then \(\text{logDeriv}(\prod _{\rho \in K} g_\rho (z)) = \sum _{\rho \in K} \text{logDeriv}(g_\rho (z))\).

LaTeX Lean

Lemma 620Uniform 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.

LaTeX Lean

Lemma 597Log 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 \]

LaTeX Lean

Lemma 598Log 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 \]

LaTeX Lean

Lemma 617Log 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 \]

LaTeX Lean

Lemma 2Square log

For \(t\ge 2\) we have \(\log (t^2) = 2\log t\)

LaTeX Lean

Lemma 252Order at least one

Let \(0{\lt}R{\lt}1\), \(R_1=\frac{2}{3}R\), and \(f:{\mathbb C}\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\). If \(f(0)\neq 0\) then \(m_{\rho ,f}\ge 1\) for all \(\rho \in \mathcal K_f(R_1)\).

LaTeX Lean

Lemma 251Order is integer

LaTeX Lean

Lemma 588Order 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)\).

LaTeX Lean

Lemma 315Max modulus

Let \(B{\gt}1\), \(0{\lt}R{\lt}1\) and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\). If \(B_f(z)\) is AnalyticOnNhd \(\overline{{\mathbb D}}_R\) and \(|B_f(z)|\le B\) for all \(|z|=R\), then \(|B_f(z)|\le B\) for all \(|z|\le R\).

LaTeX Lean

Lemma 104Interior max

Let \(R{\gt}0\). Let \(h:\overline{{\mathbb D}}_R \to {\mathbb C}\) be analytic. Suppose there exists \(w\in {\mathbb D}_R\) such that \(|h(w)| \ge |h(z)|\) for all \(z\in {\mathbb D}_R\). Then \(|h(z)|=|h(w)|\) for all \(z\in \overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 105Boundary value

LaTeX Lean

Lemma 106Boundary bound

Let \(R{\gt}0\). Let \(h:\overline{{\mathbb D}}_R \to {\mathbb C}\) be analytic. Suppose there exists \(w\in {\mathbb D}_R\) such that \(|h(w)| \ge |h(z)|\) for all \(z\in {\mathbb D}_R\). Then \(|h(R)|\ge |h(z)|\) for all \(z\in \overline{{\mathbb D}}_R\)

LaTeX Lean

Lemma 107Boundary point

Let \(R{\gt}0\). Let \(h:\overline{{\mathbb D}}_R \to {\mathbb C}\) be analytic. There exists \(v\in \overline{{\mathbb D}}_R\) with \(|v|=R\) such that \(|h(v)|\ge |h(z)|\) for all \(z\in \overline{{\mathbb D}}_R\)

LaTeX Lean

Lemma 108Boundary point

Let \(R{\gt}0\). Let \(h(z)\) be analytic on \(|z|\le R\). There exists \(v\in {\mathbb C}\) with \(|v|=R\) such that \(|h(v)|\ge |h(z)|\) for all \(z\in {\mathbb C}\) with \(|z|\le R\).

LaTeX Lean

Lemma 109Boundary max

Let \(R{\gt}0\) and \(B\ge 0\). Let \(h(z)\) be a function analytic on \(|z| \le R\). Suppose that \(|h(z)| \le B\) for all \(z\in {\mathbb C}\) with \(|z|= R\). Then there exists \(v\in {\mathbb C}\) with \(|v|=R\) such that \(|h(v)|\ge |h(w)|\) for all \(w\in {\mathbb C}\) with \(|w|\le R\), and \(|h(v)| \le B\).

LaTeX Lean

Lemma 112Maximum modulus principle

Let \(T{\gt}0\) and \(B\ge 0\). Let \(h(z)\) be a function analytic on \(|z| \le T\). We have \(|h(z)| \le B\) for all \(z\in {\mathbb C}\) with \(|z|\le T\) if and only if \(|h(z)| \le B\) for all \(z\in {\mathbb C}\) with \(|z|= T\).

LaTeX Lean

Lemma 298B at zero

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)\neq 0\). Then \(|B_f(0)|=|f(0)|\prod _{\rho \in \mathcal K_f(R_1)}\left|\frac{R}{-\rho }\right|^{m_\rho }|\).

LaTeX Lean

Lemma 304B zero form

LaTeX Lean

Lemma 302B zero form

LaTeX Lean

Lemma 313Boundary mod

Let \(R{\gt}0\) and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\). Then \(|B_f(z)|=|f(z)|\) for all \(|z|=R\).

LaTeX Lean

Lemma 294B modulus

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\). If \(\mathcal K_f(R_1)\) if finite, then \(z\in \overline{{\mathbb D}}_R\setminus \mathcal K_f(R_1)\), we have

\[ |B_f(z)|=|f(z)|\prod _{\rho \in \mathcal K_f(R_1)}\Big|\left(\frac{R-z\bar\rho /R}{z-\rho }\right)^{m_\rho }\Big| \]

LaTeX Lean

Lemma 297B modulus

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\). If \(\mathcal K_f(R_1)\) if finite, then \(|B_f(z)|=|f(z)|\prod _{\rho \in \mathcal K_f(R_1)}\left|\frac{R-z\bar\rho /R}{z-\rho }\right|^{m_\rho }\).

LaTeX Lean

Lemma 299Abs division

Let \(w_1, w_2 \in {\mathbb C}\) with \(w_2 \neq 0\). We have \(|w_1/w_2| = |w_1|/|w_2|\).

LaTeX Lean

Lemma 301Abs ratio

Let \(R{\gt}0\) and \(\rho \in {\mathbb C}\) with \(\rho \neq 0\). We have \(|\frac{R}{-\rho }| = |R|/|\rho |\).

LaTeX Lean

Lemma 311Modulus bound

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). Then \(\prod _{\rho \in \mathcal K_f(R_1)}(3/2)^{m_\rho } \ge 1\).

LaTeX Lean

Lemma 300Abs neg

Let \(w \in {\mathbb C}\). We have \(|-w| = |w|\).

LaTeX Lean

Lemma 303Abs positive

Let \(x \in {\mathbb R}\). If \(x{\gt}0\), then \(|x|=x\).

LaTeX Lean

Lemma 293Mod product

Let \(\{ w_\rho \} _{\rho \in K}\) be a finite collection of complex numbers. We have \(|\prod _{\rho \in I} w_\rho | = \prod _{\rho \in K} |w_\rho |\).

LaTeX Lean

Lemma 286Mod positive

Let \(z \in {\mathbb C}\). If \(z \neq 0\) then \(|z| {\gt} 0\).

LaTeX Lean

Lemma 287Rho positive

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\). If \(f(0)\neq 0\) then \(|\rho |{\gt}0\) for all \(\rho \in \mathcal K_f(R_1)\).

LaTeX Lean

Lemma 38Mod square

For any \(a,b \in {\mathbb R}\), we have \(|a + ib|^2 = a^2 + b^2\).

LaTeX Lean

Lemma 39Shifted mod

For any \(a,b,c \in {\mathbb R}\), we have \(|c-a - ib|^2 = (c-a)^2 + b^2\).

LaTeX Lean

Lemma 142Modulus one

For \(t\in {\mathbb R}\) we have \(|e^{it}| = e^{\Re (it)}\)

LaTeX Lean

Lemma 148Scaled modulus

For \(a{\gt}0\) and \(t\in {\mathbb R}\) we have \(|ae^{it}| = a\)

LaTeX Lean

Lemma 234Modulus of \(B(z)\) in product form

LaTeX Lean

Lemma 147Unit modulus

For \(t\in {\mathbb R}\) we have \(|e^{it}| = 1\)

LaTeX Lean

Lemma 233Modulus of \(\exp (J(z))\)

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Let \(J\) be the function from lemma 220. Then for any \(z \in \overline{{\mathbb D}}_R\),

\[ |\exp (J(z))| = \exp (\Re (J(z))). \]

LaTeX Lean

Lemma 235Modulus of \(\exp (J(z))\)

LaTeX Lean

Lemma 140Modulus of \(f'\)

Let \(0 {\lt} r {\lt} r' {\lt} R\). Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\), we have \(|f'(z)| \le \frac{1}{2\pi } \int _{0}^{2\pi } \left|\frac{f(r'e^{it}) r'e^{it}}{(r'e^{it}-z)^2} \right| \, dt\).

LaTeX Lean

Lemma 138Derivative modulus

Let \(0 {\lt} r {\lt} r' {\lt} R\). Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\), we have \(|f'(z)| = \left|\frac{1}{2\pi } \int _{0}^{2\pi } \frac{f(r'e^{it}) r'e^{it}}{(r'e^{it}-z)^2}\, dt \right|\).

LaTeX Lean

Lemma 166Integrand modulus

Let \(0 {\lt} r {\lt} r' {\lt} R\). Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\), we have \(\left|\frac{f(r'e^{it}) r'e^{it}}{(r'e^{it}-z)^2}\right| = \frac{|f(r'e^{it}) r'e^{it}|}{|(r'e^{it}-z)^2|}\).

LaTeX Lean

Lemma 141Integrand modulus

Let \(0 {\lt} r {\lt} r' {\lt} R\). Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\), we have \(|f(r'e^{it}) r'e^{it}| = |f(r'e^{it})| \cdot |r'e^{it}|\).

LaTeX Lean

Lemma 149Integrand modulus

Let \(0 {\lt} r {\lt} r' {\lt} R\). Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\), we have \(|f(r'e^{it}) r'e^{it}| = r' |f(r'e^{it})|\).

LaTeX Lean

Lemma 167Product modulus

LaTeX Lean

Lemma 168Product modulus

LaTeX Lean

Lemma 169Product modulus

Let \(0 {\lt} r {\lt} r' {\lt} R\). Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\), we have \(\frac{r'|f(r'e^{it})|}{|r'e^{it}-z|^2} \le \frac{r'|f(r'e^{it})|}{(r'-r)^2}\).

LaTeX Lean

Lemma 170Product modulus

LaTeX Lean

Lemma 150Square modulus

For any \(c \in {\mathbb C}\), \(|c^2| = |c|^2\).

LaTeX Lean

Lemma 45Modulus identity

For any \(w \in {\mathbb C}\), \(|2M-w|^2 - |w|^2 = 4M(M - \Re (w))\).

LaTeX Lean

Lemma 44Modulus diff

For any \(w \in {\mathbb C}\), \(|2M-\Re (w) - i\Im w|^2 - |\Re (w) + i\Im w|^2 = 4M(M - \Re (w))\).

LaTeX Lean

Lemma 151Shifted modulus

For any \(w,z \in {\mathbb C}\), \(|(w-z)^2| = |w-z|^2\).

LaTeX Lean

Lemma 291Mult inequality

Let \(a, b, c \in {\mathbb R}\). If \(a \le b\) and \(c {\gt} 0\), then \(ac \le bc\).

LaTeX Lean

Lemma 608Neg bound

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

LaTeX Lean

Lemma 13Exp form

For \(n\ge 1\) and \(y\in {\mathbb R}\) we have \(n^{-iy} = e^{-iy\log n}\).

LaTeX Lean

Lemma 46Nonneg product

If \(M{\gt}0\) and \(x \le M\), then \(4M(M-x) \ge 0\).

LaTeX Lean

Lemma 47Nonneg product

Let \(M{\gt}0\) and \(w\in {\mathbb C}\). If \(\Re (w) \le M\) then \(4M(M-\Re (w)) \ge 0\).

LaTeX Lean

Lemma 48Modulus compare

Let \(M{\gt}0\) and \(w \in {\mathbb C}\). If \(\Re (w) \le M\) then \(|2M-w|^2 - |w|^2 \ge 0\).

LaTeX Lean

Lemma 49Modulus bound

Let \(M{\gt}0\) and \(w \in {\mathbb C}\). If \(\Re (w) \le M\) then \(|2M-w|^2 \ge |w|^2\).

LaTeX Lean

Lemma 50Modulus bound

Let \(M{\gt}0\) and \(w \in {\mathbb C}\). If \(\Re (w) \le M\) then \(|2M-w| \ge |w|\).

LaTeX Lean

Lemma 51Modulus order

Let \(M{\gt}0\) and \(w \in {\mathbb C}\). If \(\Re (w) \le M\) then \(|w|\le |2M-w|\).

LaTeX Lean

Lemma 54Ratio bound

Let \(M{\gt}0\) and \(w \in {\mathbb C}\). If \(|2M-w|{\gt}0\) and \(|w|\le |2M-w|\) then \(\frac{|w|}{|2M-w|} \le 1\).

LaTeX Lean

Lemma 55Ratio bound

Let \(M{\gt}0\) and \(w \in {\mathbb C}\). If \(\Re (w) \le M\) and \(|w|\le |2M-w|\) then \(\frac{|w|}{|2M-w|} \le 1\).

LaTeX Lean

Lemma 56Ratio bound

Let \(M{\gt}0\) and \(w \in {\mathbb C}\). If \(\Re (w) \le M\) then \(\frac{|w|}{|2M-w|} \le 1\).

LaTeX Lean

Lemma 33Pos real nonzero

If \(w \in {\mathbb C}\) has \(\Re (w) {\gt} 0\), then \(w \neq 0\).

LaTeX Lean

Lemma 77Nonzero subset

Let \(0{\lt}R{\lt}1\) and \(V=\{ z\in \overline{{\mathbb D}}_R: z \neq 0\} \) and \(U=\{ z\in {\mathbb C}: z \neq 0\} \). Then \(V\subset U\).

LaTeX Lean

Lemma 93Outside disk bound

For \(R{\gt}0\), if \(w\notin {\mathbb D}_R\) then \(|w| \ge R\).

LaTeX Lean

Lemma 329Zeros 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\). If \(f(0)=1\) and \(|f(z)|\le B\) on \(|z|\le R\), then \(|\mathcal K_f(R_1)| \le \frac{\log B}{\log (R/R_1)}\).

LaTeX Lean

Lemma 540Exponent split

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

LaTeX Lean

Lemma 391Nonzero factor

For \(p\in \mathcal{P}\) and \(s\in {\mathbb C}\) with \(\Re (s){\gt}1\), we have \(1-p^{-s}\neq 0\).

LaTeX Lean

Lemma 72Factor power

Let \(f:{\mathbb C}\to {\mathbb C}\) be analytic at \(0\), and let \(n_0\) be the analyticOrderAt for \(f\) at \(0\). If \(n_0\in {\mathbb N}\) then there exists a nhd \(N\) of \(0\) and \(g:{\mathbb C}\to {\mathbb C}\) such that \(g\) is analytic at \(0\), and \(f(z) = z^{n_0} g(z)\) on \(N\).

LaTeX Lean

Lemma 73Factor linear

Let \(f:{\mathbb C}\to {\mathbb C}\) be analytic at \(0\), and let \(n_0\) be the analyticOrderAt for \(f\) at \(0\). If \(n_0\in {\mathbb N}\) and \(n_0\neq 0\), then there exists a nhd \(N\) of \(0\) and \(h:{\mathbb C}\to {\mathbb C}\) such that \(h\) is analytic at \(0\), and \(f(z) = zh(z)\) on \(N\).

LaTeX Lean

Lemma 74Divide zero

Let \(f:{\mathbb C}\to {\mathbb C}\) be analytic at \(0\), and let \(n_0\) be the analyticOrderAt for \(f\) at \(0\). If \(f\neq 0\) and \(f(0)=0\), then \(h(z)=f(z)/z\) is analytic at \(0\).

LaTeX Lean

Lemma 70Order nonzero

Let \(f:{\mathbb C}\to {\mathbb C}\) be analytic, and let \(n_0\) be the analyticOrderAt for \(f\) at \(0\). If \(f(0)=0\) then \(n_0 \neq 0\).

LaTeX Lean

Lemma 71Order natural

Let \(f:{\mathbb C}\to {\mathbb C}\) be analytic, and let \(n_0\) be the analyticOrderAt for \(f\) at \(0\). If \(f\neq 0\) then \(n_0 \in {\mathbb N}\).

LaTeX Lean

Lemma 385Prime decay

For \(p\in \mathcal{P}\) and \(s\in {\mathbb C}\) with \(\Re (s){\gt}1\), we have \(|p^{-s}|{\lt}1\).

LaTeX Lean

Lemma 418Sum identity

For \(s\in {\mathbb C}\), let \(f(u) = u^{-s}\) and \(a_n=1\) for all \(n\) \(N\in {\mathbb N}\). Then \(\zeta _N(s) = \sum _{n=1}^N a_n f(n)\).

LaTeX Lean

Lemma 24Trig positive

For any \(\theta \in {\mathbb R}\) we have \(0\le 3+4\cos (\theta )+\cos (2\theta )\).

LaTeX Lean

Lemma 25Trig positive

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

LaTeX Lean

Lemma 306Power bound

Let \(n \in {\mathbb N}\). If \(c {\gt} 1\) and \(n \ge 1\), then \(c \le c^n\).

LaTeX Lean

Lemma 307Power one

Let \(n \in {\mathbb N}\). If \(c \ge 1\) and \(n \ge 1\), then \(1 \le c^n\).

LaTeX Lean

Lemma 309Product one

Let \(K\) be a finite set. Then \(\prod _{\rho \in K} 1=1\).

LaTeX Lean

Lemma 305Prod inequality

Let \(K\) be a finite set, \(a:K\to {\mathbb R}\), and \(b:K\to {\mathbb R}\). If \(0\le a_\rho \le b_\rho \) for all \(\rho \in K\), then \(\prod _{\rho \in K} a_\rho \le \prod _{\rho \in K} b_\rho \).

LaTeX Lean

Lemma 409Prod order

Let \(P\) be a set, and \(a(p):P\to {\mathbb C}\) and \(b(p):P\to {\mathbb C}\) be multipliable. If \(0 {\lt} a(p) \le b(p)\) for all \(p\in P\) then \(\prod '_{p\in P} a(p) \le \prod '_{p\in P} b(p)\).

LaTeX Lean

Lemma 262Product split

Let \(f:\overline{{\mathbb D}}_1\to {\mathbb C}\) be a function that is AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)\neq 0\). For each \(\sigma \in \mathcal{K}_f(R_1)\) we have

\[ \prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}} =(z-\sigma )^{m_{\sigma ,f}}\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}} \]

LaTeX Lean

Lemma 263Product quotient

\[ \frac{(z-\sigma )^{m_{\sigma ,f}}}{\prod _{\rho \in \mathcal{K}_f(R_1)}(z-\rho )^{m_{\rho ,f}}} = \frac{1}{\prod _{\rho \in \mathcal{K}_f(R_1) \setminus \{ \sigma \} }(z-\rho )^{m_{\rho ,f}}} \]

LaTeX Lean

Lemma 396Ratio product

Let \(P\) be a set, and \(a(p):P\to {\mathbb C}\) and \(b(p):P\to {\mathbb C}\) be multipliable. Then \( \frac{\prod '_{p\in P} a(p)}{\prod '_{p\in P} b(p)} = \prod '_{p\in P} \frac{a(p)}{b(p)}\).

LaTeX Lean

Lemma 308Product power

Let \(K\) be a finite set. If \(c_{\rho } \ge 1\), \(n_\rho \in {\mathbb N}\), and \(n_{\rho } \ge 1\) for all \(\rho \in K\), then \(\prod _{\rho \in K} c_{\rho }^{n_{\rho }} \ge \prod _{\rho \in K} 1\).

LaTeX Lean

Lemma 310Power bound

Let \(K\) be a finite set. If \(c_{\rho } \ge 1\), \(n_\rho \in {\mathbb N}\), and \(n_{\rho } \ge 1\) for all \(\rho \in K\), then \(\prod _{\rho \in K} c_{\rho }^{n_{\rho }} \ge 1\).

LaTeX Lean

Lemma 116Quotient analytic

Let \(R{\gt}0\). If \(h_1(z)\) and \(h_2(z)\) are analytic for \(|z|\le R\) and \(h_2(z)\neq 0\) for all \(|z|\le R\), then \(h_1(z)/h_2(z)\) is analytic for \(|z|\le R\).

LaTeX Lean

Lemma 292Ratio bound

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\) with \(f(0)\neq 0\). If \(\rho \in \mathcal K_f(R_1)\) then \(R/|\rho |\ge R/R_1\).

LaTeX Lean

Lemma 189Sum positive

Given \(0 {\lt} r {\lt} R\), we have \(0 {\lt} R+r\).

LaTeX Lean

Lemma 178Radius compare

Given \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(r {\lt} r'\).

LaTeX Lean

Lemma 180Intermediate radius

Given \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(r {\lt} r' {\lt} R\).

LaTeX Lean

Lemma 179Radius compare

Given \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(r' {\lt} R\).

LaTeX Lean

Lemma 400Inverse ratio

For any \(z\in {\mathbb C}\). If \(|z|{\lt}1\) then \(\frac{(1-z^2)^{-1}}{(1-z)^{-1}} = (1+z)^{-1}\).

LaTeX Lean

Lemma 255Ratio analytic

Let \(w\in {\mathbb C}\), \(0{\lt}R_1{\lt}R{\lt}1\), and \(h:\overline{{\mathbb D}}_R\to {\mathbb C}\) be a function that is AnalyticAt \(w\). Let \(S \subset \overline{{\mathbb D}}_{R_1}\) be a finite set, and for each \(s \in S\), let \(n_s \in \mathbb {N}\) be a positive integer. Then for all \(w\in \overline{{\mathbb D}}_1\setminus S\), the function \(h(z)/\prod _{s \in S} (z-s)^{n_s}\) is analyticAt \(w\).

LaTeX Lean

Lemma 503Delta 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*}

LaTeX Lean

Lemma 508Double 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*}

LaTeX Lean

Lemma 504Real 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*}

LaTeX Lean

Lemma 506Inverse 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*}

LaTeX Lean

Lemma 507Scaled 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*}

LaTeX Lean

Lemma 505Positive 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*}

LaTeX Lean

Lemma 502Real 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*}

LaTeX Lean

Lemma 488Reciprocal real

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

LaTeX Lean

Lemma 393Real double

For \(s\in {\mathbb C}\) we have \(\Re (2s)=2\Re (s)\).

LaTeX Lean

Lemma 394Real bound

For \(s\in {\mathbb C}\), if \(\Re (s){\gt}1\) then \(\Re (2s){\gt}1\).

LaTeX Lean

Lemma 336Real part diff

Let \(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\) with \(f(0)=1\). Then \(\Re (L_f(z)) = \log |B_f(z)| - \log |B_f(0)|\) on \(\overline{{\mathbb D}}_{r}\).

LaTeX Lean

Lemma 341Real part bound

Let \(B{\gt}1\), \(0{\lt}r{\lt}R_1{\lt}R{\lt}1\) and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\). If \(f(0)=1\) and \(|f(z)|\le B\) on \(|z|\le R\), then \(\Re (L_f(z)) \le \log B\) for all \(|z|\le r\).

LaTeX Lean

Lemma 237Real logarithm of modulus difference

LaTeX Lean

Lemma 30Real part lower bound

For \(w\in {\mathbb C}\) and \(M{\gt}0\), if \(\Re (w) \le M\) then \(2M-\Re (w) \ge M\).

LaTeX Lean

Lemma 31Real part bound

For \(w\in {\mathbb C}\) and \(M{\gt}0\), if \(\Re (w) \le M\) then \(\Re (2M - w) \ge M\).

LaTeX Lean

Lemma 32Real part >0

For \(w\in {\mathbb C}\) and \(M{\gt}0\), if \(\Re (w) \le M\) then \(\Re (2M - w) {\gt} 0\).

LaTeX Lean

Lemma 342M minus nonzero

For \(w\in {\mathbb C}\) and \(M{\gt}0\), if \(\Re (w) \le M\) then \(2M - w\neq 0\).

LaTeX Lean

Lemma 362M minus mod

For \(w\in {\mathbb C}\) and \(M{\gt}0\), if \(\Re (w) \le M\) then \(|2M - w|{\gt}0\).

LaTeX Lean

Lemma 27Real part diff

For any \(w \in {\mathbb C}\), \(\Re (2M-w) = 2M - \Re (w)\).

LaTeX Lean

Lemma 28Real part 2M

We have \(\Re (2M-f(z)) = 2M - \Re (f(z))\).

LaTeX Lean

Lemma 6Real scale

For \(b\in {\mathbb R}\) and \(w\in {\mathbb C}\) we have \(\Re (bw) = b\Re (w)\).

LaTeX Lean

Lemma 546Real 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})\).

LaTeX Lean

Lemma 543Real terms

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

LaTeX Lean

Lemma 498Real 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})\).

LaTeX Lean

Lemma 377Rearranged deriv

\[ \frac{f'}{f}(z) - \sum _{\rho \in \mathcal K_f(R_1)}\frac{m_{\rho ,f}}{z-\rho } = L'_f(z) - \sum _{\rho \in \mathcal K_f(R_1)}\frac{m_{\rho ,f}}{z-R^2/\bar\rho }. \]

LaTeX Lean

Lemma 9Real cosine

For \(a\in {\mathbb R}\) we have \(\Re (e^{ia}) = \cos (a)\)

LaTeX Lean

Lemma 143Cosine part

For \(t\in {\mathbb R}\) we have \(\Re (it) = 0\)

LaTeX Lean

Lemma 115Removable zero

Let \(R{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\). Then the function \(h(z) = f(z)/z\) is analytic on \(|z| \le R\).

LaTeX Lean

Lemma 522Real part

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

LaTeX Lean

Lemma 576Real 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 )\).

LaTeX Lean

Lemma 583Real 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\)

LaTeX Lean

Lemma 152Reverse triangle

For any \(w, z\in {\mathbb C}\), we have \(|w|-|z| \le |w-z|\).

LaTeX Lean

Lemma 153Reverse triangle

Let \(t\in {\mathbb R}\) and \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\), we have \(|r'e^{it}|-|z| \le |r'e^{it}-z|\).

LaTeX Lean

Lemma 154Reverse triangle

Let \(t\in {\mathbb R}\) and \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\), we have \(r' -|z| \le |r'e^{it}-z|\).

LaTeX Lean

Lemma 161Reverse triangle

Let \(t\in {\mathbb R}\) and \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\) with \(|z|\le r\), we have \(0 {\lt} |r'e^{it}-z|\).

LaTeX Lean

Lemma 163Reverse triangle

Let \(t\in {\mathbb R}\) and \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\) with \(|z|\le r\), we have \(r'e^{it}-z \neq 0\).

LaTeX Lean

Lemma 164Reverse triangle

Let \(t\in {\mathbb R}\) and \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\) with \(|z|\le r\), we have \((r'e^{it}-z)^2 \neq 0\).

LaTeX Lean

Lemma 539Real converges

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

LaTeX Lean

Lemma 548Cos 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)\).

LaTeX Lean

Lemma 555Delta 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*}

LaTeX Lean

Lemma 553Delta 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*}

LaTeX Lean

Lemma 554Delta 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*}

LaTeX Lean

Lemma 549Cos series

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

LaTeX Lean

Lemma 552Zero series

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

LaTeX Lean

Lemma 550Double cos

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

LaTeX Lean

Lemma 606Real 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 )\)

LaTeX Lean

Lemma 584Gap bound

LaTeX Lean

Lemma 547Real 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})\)

LaTeX Lean

Lemma 283Disk bound

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\). If \(\rho \in \mathcal K_f(R_1)\) then \(|\rho |\le R_1\).

LaTeX Lean

Lemma 288Disk bound

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\). If \(\rho \in \mathcal K_f(R_1)\) then \(|\rho |\le R_1\).

LaTeX Lean

Lemma 285Nonzero rho

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\). If \(f(0)\neq 0\) then \(\rho \neq 0\) for all \(\rho \in \mathcal K_f(R_1)\).

LaTeX Lean

Lemma 599Real 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\)

LaTeX Lean

Lemma 527In 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\).

LaTeX Lean

Lemma 602Zero set

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

LaTeX Lean

Lemma 157Radius relation

If \(0{\lt}r{\lt}r'\) then \(r'-r{\gt}0\)

LaTeX Lean

Lemma 158Radius relation

If \(0{\lt}r{\lt}r'\) then \((r'-r)^2{\gt}0\)

LaTeX Lean

Lemma 96Positive modulus

For \(R{\gt}0\) we have \(|R|=R\).

LaTeX Lean

Lemma 97Modulus bound

For \(R{\gt}0\) we have \(|R|\le R\).

LaTeX Lean

Lemma 98Positive radius belongs to its closed disk

For \(R{\gt}0\) we have \(R\in \overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 59Scaled triangle

Let \(r{\gt}0\) and \(N,F\in {\mathbb C}\). We have \(r|N - F| \le r(|N| + |F|)\)

LaTeX Lean

Lemma 60Scaled triangle

Let \(r{\gt}0\) and \(N,F\in {\mathbb C}\). We have \(r|N - F| \le r|N| + r|F|\)

LaTeX Lean

Lemma 61Ineq step

Let \(0{\lt}r{\lt}R\) and \(N,F\in {\mathbb C}\). If \(R|F| \le r|N-F|\) then \(R|F| \le r|N| + r|F|\)

LaTeX Lean

Lemma 62Rearranged bound

Let \(0{\lt}r{\lt}R\) and \(N,F\in {\mathbb C}\). If \(R|F| \le r|N-F|\) then \((R-r)|F| \le r|N|\)

LaTeX Lean

Lemma 66Key bound

Let \(0{\lt}r{\lt}R\), \(M{\gt}0\), and \(F\in {\mathbb C}\). If \(RF \le r|2M-F|\) then \((R-r)|F| \le 2Mr\)

LaTeX Lean

Lemma 68Divide bound

Let \(0{\lt}r{\lt}R\), \(M{\gt}0\), and \(F\in {\mathbb C}\). If \((R-r)|F| \le 2Mr\) then \(|F| \le \frac{2Mr}{R-r}\).

LaTeX Lean

Lemma 69Final bound

Let \(0{\lt}r{\lt}R\), \(M{\gt}0\), and \(F\in {\mathbb C}\). If \(R|F| \le r|2M-F|\) then \(|F| \le \frac{2Mr}{R-r}\)

LaTeX Lean

Lemma 493Half 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)\).

LaTeX Lean

Lemma 437S open

Let \(S=\{ s\in {\mathbb C}: s\neq 1\} \). Then \(S\) is open.

LaTeX Lean

Lemma 492Outside zeros

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

LaTeX Lean

Lemma 449s bound

Let \(s=\sigma +it\). If \(\tfrac {1}{2} \le \sigma {\lt} 3\), then \(|s| {\lt} 3+|t|\).

LaTeX Lean

Lemma 562Series 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)) \]

LaTeX Lean

Lemma 26Series positive

For a convergent series \(r=\sum _{n=1}^\infty r_n\), if \(r_n\ge 0\) for all \(n\ge 1\), then \(r\ge 0\).

LaTeX Lean

Lemma 489Zero free

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

LaTeX Lean

Lemma 468Zero free

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

LaTeX Lean

Lemma 490Zero bound

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

LaTeX Lean

Lemma 491Zero bound

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

LaTeX Lean

Lemma 196Bound simplify

Given \(M{\gt}0\) and \(0 {\lt} r {\lt} R\), we have \(\frac{4(R+r)^2 M}{(R-r)^3} {\lt} \frac{16R^2 M}{(R-r)^3}\).

LaTeX Lean

Lemma 397Ratio split

For \(s\in {\mathbb C}\) with \(\Re (s){\gt}1\), we have \(\frac{\prod '_{p\in \mathcal{P}}(1-p^{-2s})^{-1}}{\prod '_{p\in \mathcal{P}}(1-p^{-s})^{-1}} = \prod '_{p\in \mathcal{P}}\frac{(1-p^{-2s})^{-1}}{(1-p^{-s})^{-1}}\).

LaTeX Lean

Lemma 447Inverse mod

For \(s\in {\mathbb C}, s\neq 1\), we have \(\left|\frac{1}{s-1}\right| =\frac{1}{|s-1|}\).

LaTeX Lean

Lemma 191Square fact

If \(0 {\lt} a {\lt} b\), then \(a^2 {\lt} b^2\).

LaTeX Lean

Lemma 21Square nonneg

For \(y\in {\mathbb R}\) we have \(0\le y^2\).

LaTeX Lean

Lemma 22Double square

For \(y\in {\mathbb R}\) we have \(0\le 2y^2\).

LaTeX Lean

Lemma 23Cos square

For any \(\theta \in {\mathbb R}\) we have \(0\le 2(1+\cos (\theta ))^2\).

LaTeX Lean

Lemma 327Ones 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\). If \(f(0)=1\) and \(|f(z)|\le B\) on \(|z|\le R\), then \(\sum _{\rho \in \mathcal K_f(R_1)} 1 \le \frac{\log B}{\log (R/R_1)}\).

LaTeX Lean

Lemma 328Count identity

Let \(S\) be a finite set. Then \(\sum _{s \in S} 1 = |S|\).

LaTeX Lean

Lemma 380Step two

Let \(0{\lt}R_1{\lt}R{\lt}1\) and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). Then for all \(z\in \overline{{\mathbb D}}_{R_1}\setminus \mathcal K_f(R_1)\) we have

\[ \sum _{\rho \in \mathcal K_f(R_1)}\frac{m_{\rho ,f}}{|z-R^2/\bar\rho |} \le \frac{1}{R^2/R_1 - R_1}\sum _{\rho \in \mathcal K_f(R_1)}m_{\rho ,f}. \]

LaTeX Lean

Lemma 325Sum inequality

Let \(K\) be a finite set, \(a:K\to {\mathbb R}\), and \(b:K\to {\mathbb R}\). If \(a_\rho \le b_\rho \) for all \(\rho \in K\), then \(\sum _{\rho \in K} a_\rho \le \sum _{\rho \in K} b_\rho \).

LaTeX Lean

Lemma 326Multiplicity one

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\). Then \(\sum _{\rho \in \mathcal K_f(R_1)} 1 \le \sum _{\rho \in \mathcal K_f(R_1)} m_\rho \).

LaTeX Lean

Lemma 324Multiplicity 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\). If \(f(0)=1\) and \(|f(z)|\le B\) on \(|z|\le R\), then \(\sum _{\rho \in \mathcal K_f(R_1)} m_\rho \le \frac{\log B}{\log (R/R_1)}\).

LaTeX Lean

Lemma 593Order 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)}\).

LaTeX Lean

Lemma 594Order 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|\)

LaTeX Lean

Lemma 374Sum difference

Let \(K\) be a finite set and \(a, b: K \to {\mathbb C}\). Then \(\sum _{\rho \in K} (a_\rho - b_\rho ) = \sum _{\rho \in K} a_\rho - \sum _{\rho \in K} b_\rho \).

LaTeX Lean

Lemma 375Sum rearranged

\[ \sum _{\rho \in \mathcal K_f(R_1)}m_{\rho ,f}\left( \frac{1}{z-R^2/\bar\rho } - \frac{1}{z-\rho }\right) = \sum _{\rho \in \mathcal K_f(R_1)}\frac{m_{\rho ,f}}{z-R^2/\bar\rho } - \sum _{\rho \in \mathcal K_f(R_1)}\frac{m_{\rho ,f}}{z-\rho }. \]

LaTeX Lean

Lemma 614Empty sum

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

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

LaTeX Lean

Lemma 592Sum 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 } \]

LaTeX Lean

Lemma 595Sum 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| \]

LaTeX Lean

Lemma 596Sum 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 \]

LaTeX Lean

Lemma 419Count sum

Let \(a_n=1\). For \(u\ge 1\), let \(A(u) = \sum _{n=1}^{\lfloor u \rfloor } a_n\). Then \(A(u) = \lfloor u \rfloor \).

LaTeX Lean

Lemma 7Real series

For a convergent series \(v=\sum _{n=1}^\infty v_n\) with \(v_n\in {\mathbb C}\), we have \(\Re (v) = \sum _{n=1}^\infty \Re (v_n)\).

LaTeX Lean

Lemma 544Real 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})\)

LaTeX Lean

Lemma 545Series 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})\)

LaTeX Lean

Lemma 499Sum 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*}

LaTeX Lean

Lemma 500Sum 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*}

LaTeX Lean

Lemma 509Sum 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*}

LaTeX Lean

Lemma 510Real 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*}

LaTeX Lean

Lemma 438T open

Let \(S=\{ s\in {\mathbb C}: s\neq 1\} \) and \(T=\{ s\in S : \Re (s){\gt}1/10\} \). Then \(T\) is open.

LaTeX Lean

Lemma 439T connected

Let \(S=\{ s\in {\mathbb C}: s\neq 1\} \) and \(T=\{ s\in S : \Re (s){\gt}1/10\} \). Then \(T\) is preconnected.

LaTeX Lean

Lemma 379Setup inequality

\[ \left|\frac{f'}{f}(z) - \sum _{\rho \in \mathcal K_f(R_1)}\frac{m_{\rho ,f}}{z-\rho }\right| \le |L'_f(z)| + \left|\sum _{\rho \in \mathcal K_f(R_1)}\frac{m_{\rho ,f}}{z-R^2/\bar\rho }\right|. \]

LaTeX Lean

Lemma 378Triangle sum

Let \(w_1, w_2 \in {\mathbb C}\). We have \(|w_1 - w_2| \le |w_1| + |w_2|\).

LaTeX Lean

Lemma 403Triangle abs

For any \(z\in {\mathbb C}\), we have \(|1-z| \le 1+|z|\).

LaTeX Lean

Lemma 590Triangle

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*}

LaTeX Lean

Lemma 57Triangle inequality

Let \(N,G\in {\mathbb C}\). We have \(|N + G| \le |N| + |G|\)

LaTeX Lean

Lemma 58Triangle minus

Let \(N,F\in {\mathbb C}\). We have \(|N - F| \le |N| + |F|\)

LaTeX Lean

Lemma 433Triangle int

For \(z_1, z_2 \in {\mathbb C}\), \(|z_1+z_2| \le |z_1|+|z_2|\). For an integral, \(|\int g(u)du| \le \int |g(u)|du\).

LaTeX Lean

Lemma 513Trivial bound

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

LaTeX Lean

Lemma 162Positive nonzero

For \(w\in {\mathbb C}\), if \(|w|{\gt}0\) then \(w\neq 0\).

LaTeX Lean

Lemma 37Real imaginary

For any \(w \in {\mathbb C}\), we have \(w=\Re (w) + i\Im w\).

LaTeX Lean

Lemma 601In 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)\).

LaTeX Lean

Lemma 529At one

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

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

LaTeX Lean

Lemma 531One 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. \]

LaTeX Lean

Lemma 530Real one

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

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

LaTeX Lean

Lemma 532Real 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. \]

LaTeX Lean

Lemma 533Real 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. \]

LaTeX Lean

Lemma 534Real 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. \]

LaTeX Lean

Lemma 528Zeta 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). \]

LaTeX Lean

Lemma 516Split 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*}

LaTeX Lean

Lemma 517Split 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*}

LaTeX Lean

Lemma 525Sum 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*}

LaTeX Lean

Lemma 526Real 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*}

LaTeX Lean

Lemma 515Shift 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). \]

LaTeX Lean

Lemma 535Combined 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*}

LaTeX Lean

Lemma 351Difference nonzero

Let \(0{\lt}R{\lt}1\), \(R_1=\frac{2}{3}R\), and \(f:{\mathbb C}\to {\mathbb C}\) AnalyticOnNhd \(\overline{{\mathbb D}}_1\) with \(f(0)=1\). Then for any \(\rho \in \mathcal{K}_f(R_1)\), the function \(z \mapsto z-\rho \) is never equal to zero, and differentiableAt \(z\) for all \(z\in \overline{{\mathbb D}}_{R_1}\setminus \mathcal K_f(R_1)\).

LaTeX Lean

Lemma 538Converges

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

LaTeX Lean

Lemma 284Zero excluded

Let \(0{\lt}R_1{\lt}R{\lt}1\), and \(f:{\mathbb C}\to {\mathbb C}\). If \(f(0)\neq 0\) then \(0\notin \mathcal K_f(R_1)\).

LaTeX Lean

Lemma 567Zero 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)}\).

LaTeX Lean

Lemma 244Zeros accumulate

Let \(R{\gt}0\) and \(f:\overline{{\mathbb D}}_R\to {\mathbb C}\). If \(\mathcal{K}_f(R) \subset \overline{{\mathbb D}}_R\) is infinite, then \(\mathcal{K}_f(R)\) has an accumulation point \(\rho _0 \in \overline{{\mathbb D}}_R\).

LaTeX Lean

Lemma 482Expand bound

There exists a constant \(A{\gt}1\) such that for all \(t\in {\mathbb R}\) with \(|t|{\gt}3\), \(c=3/2+it\), \(B{\gt}1\), \(0{\lt}r_1{\lt}r{\lt}R_1{\lt}R{\lt}1\), \(z\in \overline{{\mathbb D}}_{r_1}(c)\setminus \mathcal K_\zeta (R_1;c)\) we have

LaTeX Lean

Lemma 483Final expansion

Let \(0{\lt} r_1 {\lt} r {\lt} 5/6\). There exists constants \(C{\gt}1\) such that for all \(t\in {\mathbb R}\) with \(|t|{\gt}3\), \(c=3/2+it\), and \(z\in \overline{{\mathbb D}}_{r_1}(c)\setminus \mathcal K_\zeta (5/6;c)\) 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\left(\frac{1}{(r-r_1)^3} + 1\right)\log |t| \end{align*}

LaTeX Lean

Lemma 536Series 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*}

LaTeX Lean

Lemma 537Series 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*}

LaTeX Lean

Lemma 541Series 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*}

LaTeX Lean

Lemma 478Lower shift

There exists \(a{\gt}0\) such that for all \(t\in {\mathbb R}\) we have \(|\zeta (3/2+it)| \ge a\)

LaTeX Lean

Lemma 479Log lower

There exists \(A{\gt}1\) such that for all \(t\in {\mathbb R}\),

\[ \log \left(\frac{1}{|\zeta (3/2+it)|}\right) \leq A \]

LaTeX Lean

Lemma 481Upper disk

There exists \(b{\gt}1\) such that for all \(t\in {\mathbb R}\) with \(|t|{\gt}3\), letting \(c=3/2+it\), we have \(|\zeta (s)| \le b|t|\) for all \(s\in \overline{{\mathbb D}}_1(c)\).

LaTeX Lean

Lemma 480Upper pre

There exists \(b{\gt}1\) such that for all \(t\in {\mathbb R}\) we have \(|\zeta (s+3/2+it)| \le b|t|\) for all \(|s|\le 1\) and \(|t|\ge 3\).

LaTeX Lean

Lemma 413Ratio positive

We have \(\frac{\zeta (3)}{\zeta (3/2)}{\gt}0\).

LaTeX Lean

Lemma 574Expansion

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*}

LaTeX Lean

Lemma 414Fixed lower

There exists \(a{\gt}0\) such that for any \(t\in {\mathbb R}\), we have \(|\zeta (3/2+it)| \ge a\).

LaTeX Lean

Lemma 402Three halves

We have \(\frac{\zeta (3)}{\zeta (3/2)} = \prod '_{p\in \mathcal{P}}(1+p^{-3/2})^{-1}\).

LaTeX Lean

Lemma 395Zeta ratio

For \(s\in {\mathbb C}\) with \(\Re (s){\gt}1\), we have \(\frac{\zeta (2s)}{\zeta (s)} = \frac{\prod '_{p\in \mathcal{P}}(1-p^{-2s})^{-1}}{\prod '_{p\in \mathcal{P}}(1-p^{-s})^{-1}}\).

LaTeX Lean

Lemma 398Ratio form

For \(s\in {\mathbb C}\) with \(\Re (s){\gt}1\), we have \(\frac{\zeta (2s)}{\zeta (s)} = \prod '_{p\in \mathcal{P}}\frac{(1-p^{-2s})^{-1}}{(1-p^{-s})^{-1}}\).

LaTeX Lean

Lemma 591Triangle

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*}

LaTeX Lean

Lemma 467Disk analytic

Let \(t\in {\mathbb R}\) with \(|t|{\gt}1\), \(x \in {\mathbb R}\), and let \(c=x+it\). Then \(\zeta (s)\) is analyticOnNhd \(\overline{{\mathbb D}}_1(c)\).

LaTeX Lean

Lemma 464Analytic off

Let \(S=\{ s\in {\mathbb C}: s\neq 1\} \). Then \(\zeta (s)\) is analyticOnNhd \(S\).

LaTeX Lean

Lemma 436Analytic off

Let \(S=\{ s\in {\mathbb C}: s\neq 1\} \). Then \(\zeta (s)\) is analyticOnNhd \(S\).

LaTeX Lean

Lemma 443Zeta extend

Let \(S=\{ s\in {\mathbb C}: s\neq 1\} \) and \(T=\{ s\in S : \Re (s){\gt}1/10\} \). We have \(\zeta (s) = 1+\frac{1}{s-1} - s \int _1^\infty \{ u\} u^{-s-1} du\) on \(T\).

LaTeX Lean

Lemma 444First bound

For \(\Re (s){\gt}0, s\neq 1\),

\[ |\zeta (s)| \le 1+\left|\frac{1}{s-1}\right| + |s| \int _1^\infty |\{ u\} u^{-s-1}| du. \]

LaTeX Lean

Lemma 446Second bound

For \(\Re (s){\gt}0, s\neq 1\),

\[ |\zeta (s)| \le 1+\left|\frac{1}{s-1}\right| + \frac{|s|}{\Re (s)}. \]

LaTeX Lean

Lemma 448Third bound

For \(\Re (s){\gt}0, s\neq 1\),

\[ |\zeta (s)| \le 1 + \frac{1}{|s-1|} + \frac{|s|}{\Re (s)}. \]

LaTeX Lean

Lemma 616Center bound

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

LaTeX Lean

Lemma 469Point nonzero

For all \(t\in {\mathbb R}\) we have \(\zeta (3/2+it)\neq 0\)

LaTeX Lean

Lemma 458Diff off pole

Let \(S=\{ s\in {\mathbb C}: s\neq 1\} \). For all \(s\in S\) we have \(\zeta (s)\) DifferentiableAt \(s\).

LaTeX Lean

Lemma 386Euler product

For \(s\in {\mathbb C}\) with \(\Re (s){\gt}1\), the function \(w_s(p)=(1-p^{-s})^{-1}\) is multipliable, and we have \(\zeta (s) = \prod '_{p\in \mathcal{P}}(1-p^{-s})^{-1}\).

LaTeX Lean

Lemma 435Zeta formula

For \(\Re (s){\gt}1\),

\[ \zeta (s) = 1+\frac{1}{s-1} - s \int _1^\infty \{ u\} u^{-s-1} du. \]

LaTeX Lean

Lemma 441Analytic ext

Let \(S=\{ s\in {\mathbb C}: s\neq 1\} \) and \(T=\{ s\in S : \Re (s){\gt}1/10\} \). The function \(F(z) = \frac{z}{z-1} - z \int _1^\infty \{ u\} u^{-z-1} du\) is analyticOnNhd \(T\).

LaTeX Lean

Lemma 415Series form

For \(s\in {\mathbb C}\) with \(\Re (s){\gt}1\), we have \(\zeta (s) = \sum _{n=1}^\infty n^{-s}\).

LaTeX Lean

Lemma 428Final form

For \(s\in {\mathbb C}, s\neq 1\) and integer \(N\ge 1\),

\[ \zeta _N(s) = \frac{N^{1-s}}{1-s} + 1+\frac{1}{s-1} - s \int _1^N \{ u\} u^{-s-1} du. \]

LaTeX Lean

Lemma 423First form

For \(s\in {\mathbb C}\) and integer \(N\ge 1\),

\[ \zeta _N(s) = N^{1-s} + s \int _1^N \lfloor u \rfloor u^{-s-1} du. \]

LaTeX Lean

Lemma 426Second form

For \(s\in {\mathbb C}\) and integer \(N\ge 1\),

\[ \zeta _N(s) = N^{1-s} + s \int _1^N u^{-s} du - s \int _1^N \{ u\} u^{-s-1} du. \]

LaTeX Lean

Lemma 412Zeta positive

For \(x\in {\mathbb R}\), if \(x{\gt}1\) then \(\zeta (x)\in {\mathbb R}\) and \(\zeta (x){\gt}0\).

LaTeX Lean

Lemma 454Upper bound

For all \(z\in {\mathbb C}\) with \(\tfrac {1}{2} \le \Re (z) {\lt} 3\) and \(|\Im (z)|\ge 1\), we have \(|\zeta (z)| {\lt} 8+2|\Im (z)|\).

LaTeX Lean

Lemma 457Global bound

There exists \(b{\gt}1\) such that for all \(t\in {\mathbb R}\) we have \(|\zeta (s+3/2+it)| \le 8+2|t|\) for all \(|s|\le 1\) and \(|t|\ge 3\).

LaTeX Lean

Lemma 619Zero-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|\).

LaTeX Lean

Lemma 571Zero free

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

LaTeX Lean

Lemma 572Disk 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)\).

LaTeX Lean

Lemma 573Not 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)\).

LaTeX Lean

Lemma 455Shift calc

For \(s\in {\mathbb C}\), \(t\in {\mathbb R}\) let \(z=s+3/2+it\). Then \(\Re (z) = \Re (s)+3/2\) and \(\Im (z)=\Im (s)+t\).

LaTeX Lean

Lemma 456Shift cond

For \(s\in {\mathbb C}\), \(t\in {\mathbb R}\) let \(z=s+3/2+it\). If \(|s|\le 1\) and \(|t|\ge 3\), then \(\Re (z) \in [1/2, 3]\) and \(|\Im (z)|\ge 1\)

LaTeX Lean

Lemma 604Real 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)|\)

LaTeX Lean

Lemma 605Real 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\).

LaTeX Lean

Lemma 607Real 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\)

LaTeX Lean

Lemma 612Real 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 \).

LaTeX Lean

Lemma 155Radius relation

Let \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\) with \(|z|\le r\). Then \(0{\lt}r' - |z|\).

LaTeX Lean

Lemma 156Radius relation

Let \(t\in {\mathbb R}\) and \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\) and \(z\in {\mathbb C}\) with \(|z|\le r\). Then \(r' - r \le |r'e^{it}-z|\).

LaTeX Lean

Lemma 159Radius relation

Let \(t\in {\mathbb R}\) and \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\)and \(z\in {\mathbb C}\) with \(|z|\le r\). Then \((r' - r)^2 \le |r'e^{it}-z|^2\).

LaTeX Lean

Lemma 160Radius relation

Let \(t\in {\mathbb R}\) and \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\)and \(z\in {\mathbb C}\) with \(|z|\le r\). Then \(|(r'e^{it}-z)^2| = |r'e^{it}-z|^2\).

LaTeX Lean

Lemma 542Series converges

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

LaTeX Lean

Lemma 487Finite set

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

LaTeX Lean

Lemma 67Nonneg factor

Let \(0{\lt}r{\lt}R\) and \(F\in {\mathbb C}\). Then we have \((R-r)|F| \ge 0\)

LaTeX Lean

Theorem 621Strong PNT

We have

\[ \sum _{n \leq x} \Lambda (n) = x + O(x \exp (-c(\log x)^{1/2})). \]

LaTeX Lean

Theorem 198Borel-Carathéodory II

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(0{\lt}r {\lt} R\) and any \(|z|\le r\),

\[ |f'(z)| \le \frac{16M R^2}{(R-r)^3}. \]

LaTeX Lean

Theorem 133Borel-Carathéodory I

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(0{\lt}r {\lt} R,\)

\[ \sup _{|z| \le r} |f(z)| \le \frac{2r}{R-r}M. \]

LaTeX Lean

Theorem 618Bound 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. \]

LaTeX Lean

Theorem 411Zeta lower

For any \(t\in {\mathbb R}\), we have \(|\zeta (3/2+it)| \ge \frac{\zeta (3)}{\zeta (3/2)}\).

LaTeX Lean

Theorem 401Ratio identity

For \(s\in {\mathbb C}\) with \(\Re (s){\gt}1\), we have \(\frac{\zeta (2s)}{\zeta (s)} = \prod '_{p\in \mathcal{P}}(1+p^{-s})^{-1}\).

LaTeX Lean