JBlaschkeDerivBound to DeltaRange
TheoremJBlaschkeDerivBound#
Let \(B>1\) and \(0 < r' < r < R<1\). If \(f:\mathbb{C}\to\mathbb{C}\) is a function analytic on neighborhoods of points in \(\overline{\mathbb{D}_1}\) with \(f(0)=1\) and \(|f(z)|\leq B\) for all \(|z|\leq R\), then for all \(|z|\leq r'\)
Proof
By Lemma DiskBound we immediately know that \(|B_f(z)|\leq B\) for all \(|z|\leq R\). Now since \(L_f=J_{B_f}\) by Definition JBlaschke, by Theorem LogOfAnalyticFunction we know that
for all \(|z|\leq r\). Note that in the above
because of Lemma norm-fOfZero-le-norm-BlaschkeOfZero. So by Theorem BorelCaratheodoryDeriv, it follows that
for all \(|z|\leq r'\).
Lean
Formalized as JBlaschkeDerivBound.
Sources
Uses 9 · Used by 1
TheoremFinalBound#
Let \(B>1\) and \(0 < r' < r < R' < R<1\). If \(f:\mathbb{C}\to\mathbb{C}\) is a function analytic on neighborhoods of points in \(\overline{\mathbb{D}_1}\) with \(f(0)=1\) and \(|f(z)|\leq B\) for all \(|z|\leq R\), then for all \(z\in\overline{\mathbb{D}_{r'}}\setminus\mathcal{K}_f(R')\) we have
Proof
Since \(z\in\overline{\mathbb{D}_{r'}}\setminus\mathcal{K}_f(R')\) we know that \(z\not\in\mathcal{K}_f(R')\); thus, by Definition CFunction we know that
Substituting this into Definition BlaschkeB we have that
Taking the complex logarithm of both sides we have that
Taking the derivative of both sides we have that
By Definition JBlaschke and Theorem LogOfAnalyticFunction, since \(L_f(z)=J_{B_f}(z)\) we have \(L_f'(z)=J'_{B_f}(z)=(B_f'/B_f)(z)\). Thus,
Now since \(z\in\overline{\mathbb{D}_{r'}}\subseteq\overline{\mathbb{D}_{R'}}\) and \(\rho\in\mathcal{K}_f(r)\subseteq\mathcal{K}_f(R')\), we know that \(R^2/R'-R'\leq|z-R^2/\overline{\rho}|\). Thus by the triangle inequality we have
Now by Theorem ZerosBound and JBlaschkeDerivBound we get our desired result with a little algebraic manipulation.
Lean
Formalized as FinalBound.
Sources
Uses 10 · Used by 1
TheoremZetaFixedLowerBound#
For all \(t\in\mathbb{R}\) one has
Proof
From the Euler product expansion of \(\zeta\), we have that for \(\Re s>1\)
Thus, we have that
Now note that \(|1-p^{-(3/2+it)}|\leq 1+|p^{-(3/2+it)}|=1+p^{-3/2}\). Thus,
for all \(t\in\mathbb{R}\) as desired.
Lean
Formalized as ZetaFixedLowerBound.
Sources
Used by 2
DefinitionriemannZeta1#
Let
Used by 3
TheoremZeta1AltFormula#
We have that
where \(\zeta_0(1,s)\) comes from Definition riemannZeta0.
Proof
Note that
With minor simplifications we have
The first integral evaluates to \(1/s\) (when \(0\lt \mathfrak{R}s\)), so this term when multiplied by the \(s/2\) cancels with the \(-1/2\). This exactly gives \(\zeta_1\).
Lean
Formalized as Zeta1AltFormula.
Sources
Uses 2 · Used by 1
TheoremZetaAltFormula#
We have that
for all \(s\in S\) with \(S=\{s\in\mathbb{C}:0\lt \mathfrak{R}s,\,s\neq 1\}\).
Proof
This immediately follows from Lemmas Zeta1AltFormula and Zeta0EqZeta.
Lean
Formalized as ZetaAltFormula.
Sources
Uses 4 · Used by 1
TheoremGlobalBound#
For all \(s\in\mathbb{C}\) with \(|s|\leq 1\) and \(t\in\mathbb{R}\) with \(|t|\geq 2\), we have that
Proof
For the sake of clearer proof writing let \(z=s+3/2+it\). Since \(|s|\leq 1\) we know that \(1/2\leq\mathfrak{R}z\); additionally, as \(|t|\geq 2\), we know \(1\leq|\mathfrak{I}z|\). So, \(z\in S\). Thus, from Lemma ZetaAltFormula we know that
by applying the triangle inequality. Now note that \(|z-1|\geq 1\). Likewise,
Thus we have that,
Lean
Formalized as GlobalBound.
Sources
Uses 2 · Used by 2
Theoremnorm-zeta-strict-mono-ofReal#
If \(a,b\in\mathbb{R}\) with \(1\lt b\lt a\), then
Proof
Expand out \(\zeta\) as a summation (we can do this as we are in the region of convergence) and ignore the norm as every term is positive and real. Comparing term by term proves the result.
Lean
Formalized as norm_zeta_strict_mono_ofReal.
Sources
Used by 2
TheoremLogDerivZetaFinalBound#
Let \(t\in\mathbb{R}\) with \(|t|\geq 2\) and \(0 < r' < r < R' < R<1\). If \(f(z)=\zeta(z+3/2+it)\), then for all \(z\in\overline{\mathbb{D}_{r'}}\setminus\mathcal{K}_f(R')\) we have that
Proof
Let \(g(z)=\zeta(z+3/2+it)/\zeta(3/2+it)\). Note that \(g(0)=1\) and for \(|z|\leq R\)
by Theorems ZetaFixedLowerBound and GlobalBound. Thus by Theorem FinalBound we have that
Now note that \(f'/f=g'/g\), \(\mathcal{K}_f(r)=\mathcal{K}_g(r)\), and \(m_g(\rho)=m_f(\rho)\) for all \(\rho\in\mathcal{K}_f(r)\). Thus we have that,
where the implied constant \(C\) is taken to be
Lean
Formalized as LogDerivZetaFinalBound.
Sources
Uses 5 · Used by 2
TheoremZetaShiftFiniteZeros#
For all \(|t|\geq 2\), if \(f(z)=\zeta(z+3/2+it)\), then \(f(z)\) has a finite number of zeros in \(\overline{\mathbb{D}_1}\).
Proof
If we suppose the opposite, i.e. that there are an infinite number of zeros in this region, then \(f\equiv 0\) by the identity theorem. This is a contradiction, so the statement must be true.
Lean
Formalized as ZetaShiftFiniteZeros.
Sources
Uses 1 · Used by 3
DefinitionZeroWindow#
Let \(\mathcal{Z}_t=\{\rho\in\mathbb{C}:\zeta(\rho)=0,\,|\rho-(3/2+it)|\leq 3/4\}\).
Used by 8
TheoremSumBoundI#
For all \(\delta\in (0,1)\) and \(t\in\mathbb{R}\) with \(|t|\geq 2\) we have
Proof
We apply Theorem LogDerivZetaFinalBound where \(r'=2/3\), \(r=3/4\), \(R'=4/5\), and \(R=5/6\). Thus, for all \(z\in\overline{\mathbb{D}_{2/3}}\setminus\mathcal{K}_f(4/5)\) we have that
where \(f(z)=\zeta(z+3/2+it)\) for \(t\in\mathbb{R}\) with \(|t|\geq 2\). Now if we let \(z=-1/2+\delta\), then \(z\in(-1/2,1/2)\subseteq\overline{\mathbb{D}_{2/3}}\). Additionally, \(f(z)=\zeta(1+\delta+it)\), where \(1+\delta+it\) lies in the zero-free region where \(\sigma>1\). Thus, \(z\not\in\mathcal{K}_f(4/5)\). So,
But now note that if \(\rho\in\mathcal{K}_f(3/4)\), then \(\zeta(\rho+3/2+it)=0\) and \(|\rho|\leq 3/4\). Thus, \(\rho+3/2+it\in\mathcal{Z}_t\) (the argument works in reverse as well). Additionally, note that \(m_f(\rho)=m_\zeta(\rho+3/2+it)\). So changing variables using these facts gives us that
Lean
Formalized as SumBoundI.
Sources
Uses 4 · Used by 2
TheoremShiftTwoBound#
For all \(\delta\in (0,1)\) and \(t\in\mathbb{R}\) with \(|t|\geq 2\) we have
Proof
Note that, for \(\rho\in\mathcal{Z}_{2t}\)
Now since \(\rho\in\mathcal{Z}_{2t}\), we have that \(|\rho-(3/2+2it)|\leq 3/4\). So, we have \(\Re \rho\in[3/4,9/4]\) and \(\mathfrak{I}\rho\in[2t-3/4,2t+3/4]\). Additionally, we know that \(\zeta(\rho)=0\). This implies the stronger condition that \(\Re \rho\in[3/4,1]\). Thus,
Which implies that
Note that, from Lemma SumBoundI, we have
Since \(m_\zeta(\rho)\geq 0\) for all \(\rho\in\mathcal{Z}_{2t}\), the inequality from Equation (4) tells us that by subtracting the sum from both sides we have
Noting that \(\log|2t|=\log(2)+\log|t|\leq2\log|t|\) completes the proof.
Lean
Formalized as ShiftTwoBound.
Sources
Uses 2 · Used by 1
TheoremShiftOneBound#
There exists \(C>0\) such that for all \(\delta\in(0,1)\) and \(t\in\mathbb{R}\) with \(|t|\geq 2\); if \(\zeta(\rho)=0\) with \(\rho=\sigma+it\), then
Proof
Note that for \(\rho'\in\mathcal{Z}_t\)
Now since \(\rho'\in\mathcal{Z}_t\), we have that \(|\rho'-(3/2+it)|\leq 3/4\). So, we have \(\mathfrak{R}\rho'\in[3/4,9/4]\) and \(\mathfrak{I}\rho'\in[t-3/4,t+3/4]\). Additionally, we know that \(\zeta(\rho')=0\). This implies the stronger condition that \(\mathfrak{R}\rho'\in[3/4,1]\). Thus,
Which implies that
Note that, from Lemma SumBoundI, we have
Now we proceed via cases. If \(\rho\in\mathcal{Z}_t\), then \(\mathcal{Z}_t=\rho\sqcup(\mathcal{Z}_t\setminus\rho)\) and the inequality from Equation (5) tells us that by subtracting the sum over all \(\rho'\in\mathcal{Z}_t\setminus\{\rho\}\) from both sides we have
But of course we have that \(\mathfrak{R}(1+\delta+it-\rho)=1+\delta-\sigma\). So subtracting this term from both sides and recalling the implied constant we have
We have that \(\sigma\leq 1\) since \(\zeta\) is zero free on the right half plane \(\sigma>1\). Thus, \(0<1+\delta-\sigma\). Noting this in combination with the fact that \(1\leq m_\zeta(\rho)\) gives us that
Now if \(\rho\not\in\mathcal{Z}_t\), then \(|\sigma-3/2|=|\rho-(3/2+it)|>3/4\) since \(\zeta(\rho)=0\). Additionally, \(\sigma\leq 1\) since \(\zeta(\rho)=0\), thus \(3/2-\sigma=|\sigma-3/2|>3/4\). So it follows that
Thus, by subtracting the sum over \(\rho'\in\mathcal{Z}_t\) from both sides we have
Lean
Formalized as ShiftOneBound.
Sources
Uses 2 · Used by 1
TheoremShiftZeroBound#
For all \(\delta\in(0,1)\) we have
Proof
From Theorem riemannZetaLogDerivResidue we know that
Changing variables \(s\mapsto 1+\delta\) and applying the triangle inequality we have that
Lean
Formalized as ShiftZeroBound.
Sources
Uses 2 · Used by 1
TheoremvonMangoldtLSeriesSummable#
The series
converges when \(1\lt \mathfrak{R}(s)\).
Proof
We know that \(\Lambda(n)\) is \(O(n^\varepsilon)\) since it is bounded above by \(\log(n)\). Thus,
Since \(\varepsilon\) can be arbitrarily small, we know the left hand side converges by the \(p\)-test.
Lean
Formalized as vonMangoldtLSeriesSummable.
Sources
Used by 2
TheoremZeroWindowFinite#
For all \(|t|\geq 2\), \(\mathcal{Z}(t)\) contains a finite number of points.
Proof
If we suppose the opposite, i.e. that there are an infinite number of zeta zeros in this region, then \(\zeta\equiv 0\) by the identity theorem. This is a contradiction, so the statement must be true.
Lean
Formalized as ZeroWindowFinite.
Sources
Uses 1 · Used by 2
TheoremZeroInequality#
There exists a constant \(0 < E<1/14\) such that for all \(\rho=\sigma+it\) with \(\zeta(\rho)=0\) and \(|t|\geq 2\), one has
Proof
From Theorem LogDerivativeDirichlet when \(\Re s>1\) we have
Thus,
Now applying Euler's identity
Since
we know that the series on the right hand side is bounded below by \(0\), and by Lemmas ShiftTwoBound, ShiftOneBound, and ShiftZeroBound we have an upper bound on the left hand side. So,
where \(A\), \(B\), and \(C\) are the implied constants coming from Lemmas ShiftZeroBound, ShiftOneBound, and ShiftTwoBound respectively. By choosing \(D\geq 5A+4B+C\geq 3A/\log 2+4B+C\) we have
by some manipulation. Now if we choose \(\delta=(2D\log|t|)^{-1}\) then we have
So with some manipulation we have that
This is exactly the desired result with the constant \(E=(14D)^{-1}\). Since \(D\geq 5A+4B+C\geq 1\) we have that \(E\in(0,1/14)\).
Lean
Formalized as ZeroInequality.
Sources
Uses 7 · Used by 7
DefinitionDeltaT#
Let \(\delta_t=E/\log|t|\) where \(E\) is the constant coming from Theorem ZeroInequality.
Uses 1 · Used by 4
TheoremDeltaRange#
For all \(t\in\mathbb{R}\) with \(|t|\geq 2\) we have that
Proof
Note that \(\delta_t=E/\log|t|\) where \(E\) is the implied constant from Lemma ZeroInequality. But we know that \(E=(14D)^{-1}\) where \(D\geq 5A+4B+C\) where \(A\), \(B\), and \(C\) are the constants coming from Lemmas ShiftZeroBound, ShiftOneBound, and ShiftTwoBound respectively. Thus,
But note that \(A\geq 1\), \(B>0\), and \(C>0\) by Lemmas ShiftZeroBound, ShiftOneBound, and ShiftTwoBound respectively. So, by a very lazy estimate we have \(E\leq 1/14\). Thus,
Lean
Formalized as DeltaRange.
Sources
Uses 2 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.