8 Zeta function estimates
8.1 Definitions
\(\rho \) is understood to lie in the set \(\{ s: \zeta (s)=0\} \), counted with multiplicity. We will often restrict the zeroes \(\rho \) to a rectangle \(\{ \Re \rho \in I, \Im \rho \in J \} \), for instance through sums of the form \(\sum _{\Re \rho \in I, \Im \rho \in J} f(\rho )\).
We say that the Riemann hypothesis has been verified up to height \(T\) if there are no zeroes in the rectangle \(\{ \Re \rho \in (0.5, 1), \Im \rho \in [0,T] \} \).
We say that one has a classical zero-free region with parameter \(R\) if \(zeta(s)\) has no zeroes in the region \(Re(s) \geq 1 - 1 / R * \log |\Im s|\) for \(\Im (s) {\gt} 3\).
The number of zeroes of imaginary part between 0 and T, counting multiplicity
An estimate of the form \(N(T) - \frac{T}{2\pi } \log \frac{T}{2\pi e} + \frac{7}{8}| \leq b_1 \log T + b_2 \log \log T + b_3\) for \(T \geq 2\).
An estimate of the form \(N(\sigma ,T) \leq c₁ T^p \log ^q T + c₂ \log ^2 T - \frac{T}{2\pi } \log \frac{T}{2\pi e} + \frac{7}{8}| \leq b_1 \log T + b_2 \log \log T + b_3\) for \(T \geq 2\).
8.2 The estimates of Kadiri, Lumley, and Ng
In this section we establish the primary results of [ 31 ] .
8.3 The zeta function bounds of Rosser and Schoenfeld
In this section we formalize the zeta function bounds of Rosser and Schoenfeld.
One has a Riemann von Mangoldt estimate with parameters 0.137, 0.443, and 1.588.
8.4 Approximating the Riemann zeta function
We want a good explicit estimate on
for \(a\) a half-integer. As it turns out, this is the same problem as that of approximating \(\zeta (s)\) by a sum \(\sum _{n\leq a} n^{-s}\). This is one of the two 1 main, standard ways of approximating \(\zeta (s)\).
The non-explicit version of the result was first proved in [ 25 , Lemmas 1 and 2 ] . The proof there uses first-order Euler-Maclaurin combined with a decomposition of \(\lfloor x\rfloor - x +1/2\) that turns out to be equivalent to Poisson summation. The exposition in [ 47 , § 4.7–4.11 ] uses first-order Euler-Maclaurin and van de Corput’s Process B; the main idea of the latter is Poisson summation.
There are already several explicit versions of the result in the literature. In [ 8 ] , [ 29 ] and [ 45 ] , what we have is successively sharper explicit versions of Hardy and Littlewood’s original proof. The proof in [ 16 , Lemma 2.10 ] proceeds simply by a careful estimation of the terms in high-order Euler-Maclaurin; it does not use Poisson summation. Finally, [ 13 ] is an explicit version of [ 47 , § 4.7–4.11 ] ; it gives a weaker bound than [ 45 ] or [ 16 ] . The strongest of these results is [ 45 ] .
We will give another version here, in part because we wish to relax conditions – we will work with \(\left|\Im s\right| {\lt} 2\pi a\) rather than \(\left|\Im s\right| \leq a\) – and in part to show that one can prove an asymptotically optimal result easily and concisely. We will use first-order Euler-Maclaurin and Poisson summation. We assume that \(a\) is a half-integer; if one inserts the same assumption into [ 16 , Lemma 2.10 ] , one can improve the result there, yielding an error term closer to the one here.
For additional context, see the Zulip discussion at https://leanprover.zulipchat.com/#narrow/channel/423402-PrimeNumberTheorem.2B/ topic/Let.20us.20formalize.20an.20appendix
We recall that \(e(\alpha ) = e^{2\pi i \alpha }\).
8.4.1 The decay of a Fourier transform
Our first objective will be to estimate the Fourier transform of \(t^{-s} \mathbb {1}_{[a,b]}\). In particular, we will show that, if \(a\) and \(b\) are half-integers, the Fourier cosine transform has quadratic decay when evaluated at integers. In general, for real arguments, the Fourier transform of a discontinuous function such as \(t^{-s} \mathbb {1}_{[a,b]}\) does not have quadratic decay.
Let \(s = \sigma + i \tau \), \(\sigma \geq 0\), \(\tau \in \mathbb {R}\). Let \(\nu \in \mathbb {R}\setminus \{ 0\} \), \(b{\gt}a{\gt}\frac{|\tau |}{2\pi |\nu |}\). Then
where \(\varphi _\nu (t) = \nu t - \frac{\tau }{2\pi } \log t\).
We write \(t^{-s} e(\nu t) = t^{-\sigma } e(\varphi _\nu (t))\) and integrate by parts with \(u = t^{-\sigma }/(2\pi i \varphi _\nu '(t))\), \(v = e(\varphi _\nu (t))\). Here \(\varphi _\nu '(t) = \nu - \tau /(2\pi t)\ne 0\) for \(t\in [a,b]\) because \(t\geq a {\gt} |\tau |/(2\pi |\nu |)\) implies \(|\nu |{\gt}|\tau |/(2\pi t)\). Clearly
while
Let \(g:[a,b]\to \mathbb {R}\) be continuous, with \(|g(t)|\) non-increasing. Then \(g\) is monotone, and \(\| g\| _{\mathrm{TV}} = |g(a)|-|g(b)|\).
Suppose \(g\) changed sign: \(g(a'){\gt}0{\gt}g(b')\) or \(g(a') {\lt}0 {\lt} g(b')\) for some \(a\leq a'{\lt} b'\leq b\). By IVT, there would be an \(r\in [a',b']\) such that \(g(r)=0\). Since \(|g|\) is non-increasing, \(g(b')=0\); contradiction. So, \(g\) does not change sign: either \(g\leq 0\) or \(g\geq 0\).
Thus, there is an \(\varepsilon \in \{ -1,1\} \) such that \(g(t) = \varepsilon |g(t)|\) for all \(t\in [a,b]\). Hence, \(g\) is monotone. Then \(\| g\| _{\mathrm{TV}} = |g(a)-g(b)|\). Since \(|g(a)|\geq |g(b)|\) and \(g(a)\), \(g(b)\) are either both non-positive or non-negative, \(|g(a)-g(b)| = |g(a)|-|g(b)|\).
Let \(\varphi :[a,b]\to \mathbb {R}\) be \(C^1\) with \(\varphi '(t)\ne 0\) for all \(t\in [a,b]\). Let \(h:[a,b]\to \mathbb {R}\) be such that \(g(t) = h(t)/\varphi '(t)\) is continuous and \(|g(t)|\) is non-increasing. Then
Since \(\varphi \) is \(C^1\), \(e(\varphi (t))\) is \(C^1\), and \(h(t) e(\varphi (t)) = \frac{h(t)}{2\pi i \varphi '(t)} \frac{d}{dt} e(\varphi (t))\) everywhere. By Lemma 8.4.2, \(g\) is of bounded variation. Hence, we can integrate by parts:
The first term on the right has absolute value \(\leq \frac{|g(a)|+|g(b)|}{2\pi }\). Again by Lemma 8.4.2,
We are done by \(\frac{|g(a)|+|g(b)|}{2\pi } + \frac{|g(a)|-|g(b)|}{2\pi } = \frac{|g(a)|}{\pi }\).
Let \(\sigma \geq 0\), \(\tau \in \mathbb {R}\), \(\nu \in \mathbb {R}\setminus \{ 0\} \). Let \(b{\gt}a{\gt}\frac{|\tau |}{2\pi |\nu |}\). Then, for any \(k\geq 1\), \(f(t) = t^{-\sigma -k} |2\pi \nu -\tau /t|^{-k-1}\) is decreasing on \([a,b]\).
Let \(a\leq t\leq b\). Since \(\left|\frac{\tau }{t \nu }\right| {\lt} 2\pi \), we see that \(2\pi -\frac{\tau }{\nu t} {\gt}0\), and so \(|2\pi \nu -\tau /t|^{-k-1} = |\nu |^{-k-1} \left(2\pi - \frac{\tau }{t \nu }\right)^{-k-1}\). Now we take logarithmic derivatives:
since, again by \(\frac{|\tau |}{t |\nu |} {\lt} 2\pi \) and \(k\geq 1\), we have \(2\pi k + \frac{\tau }{t \nu }{\gt}0\), and, as we said, \(2\pi - \frac{\tau }{t \nu }{\gt}0\).
Let \(s = \sigma + i \tau \), \(\sigma \geq 0\), \(\tau \in \mathbb {R}\). Let \(\nu \in \mathbb {R}\setminus \{ 0\} \), \(b{\gt}a{\gt}\frac{|\tau |}{2\pi |\nu |}\). Then
where \(\varphi _\nu (t) = \nu t - \frac{\tau }{2\pi } \log t\) and \(\vartheta = \frac{\tau }{2\pi a}\).
Apply Lemma 8.4.1. Since \(\varphi _\nu '(t) = \nu - \tau /(2\pi t)\), we know by Lemma 8.4.4 (with \(k=1\)) that \(g_1(t) = \frac{t^{-\sigma -1}}{(\varphi _\nu '(t))^2}\) is decreasing on \([a,b]\). We know that \(\varphi _\nu '(t)\ne 0\) for \(t\geq a\) by \(a{\gt}\frac{|\tau |}{2\pi |\nu |}\), and so we also know that \(g_1(t)\) is continuous for \(t\geq a\). Hence, by Lemma 8.4.3,
since \(\varphi _\nu '(a) = \nu - \vartheta \). We remember to include the factor of \(\sigma \) in front of an integral in 1.
Since \(\varphi _\nu '(t)\) is as above and \(\varphi _\nu ''(t) = \tau /(2\pi t^2)\), we know by Lemma 8.4.4 (with \(k=2\)) that \(g_2(t) = \frac{t^{-\sigma } |\varphi _\nu ''(t)|}{|\varphi _\nu '(t)|^3} = \frac{|\tau |}{2\pi } \frac{t^{-\sigma -2}}{|\varphi _\nu '(t)|^3}\) is decreasing on \([a,b]\) we also know, as before, that \(g_2(t)\) is continuous. Hence, again by Lemma 8.4.3,
Let \(s = \sigma + i \tau \), \(\sigma ,\tau \in \mathbb {R}\). Let \(n\in \mathbb {Z}_{{\gt}0}\). Let \(a,b\in \mathbb {Z} + \frac{1}{2}\), \(b{\gt}a{\gt}\frac{|\tau |}{2\pi n}\). Write \(\varphi _\nu (t) = \nu t - \frac{\tau }{2\pi } \log t\). Then
Since \(e(\varphi _\nu (t)) = e(\nu t) t^{-i \tau } = (-1)^{\nu } t^{-i \tau }\) for any half-integer \(t\) and any integer \(\nu \),
for \(\nu = \pm n\). Clearly \((-1)^{\nu } = (-1)^n\). Since \(\varphi _\nu '(t) = \nu - \alpha \) for \(\alpha = \frac{\tau }{2\pi t}\),
It is this easy step that gives us quadratic decay on \(n\). It is just as in the proof of van der Corput’s Process B in, say, [ 46 , I.6.3, Thm. 4 ] .
Let \(s = \sigma + i \tau \), \(\sigma \geq 0\), \(\tau \in \mathbb {R}\). Let \(a,b\in \mathbb {Z} + \frac{1}{2}\), \(b{\gt}a{\gt}\frac{|\tau |}{2\pi }\). Write \(\vartheta = \frac{\tau }{2\pi a}\). Then, for any integer \(n\geq 1\),
Write \(\cos 2\pi n t = \frac{1}{2} (e(n t) + e(-n t))\). Since \(n\geq 1\) and \(a{\gt}\frac{|\tau |}{2\pi }\), we know that \(a{\gt}\frac{|\tau |}{2 \pi n}\), and so we can apply Lemma 8.4.5 with \(\nu = \pm n\). We then apply Lemma 8.4.6 to combine the boundary contributions \(\left. \right|_a^b\) for \(\nu =\pm n\).
8.4.2 Approximating zeta(s)
We start with an application of Euler-Maclaurin.
Let \(b{\gt}0\), \(b\in \mathbb {Z}\). Then, for all \(s\in \mathbb {C}\setminus \{ 1\} \) with \(\Re s {\gt} 0\),
Assume first that \(\Re s {\gt} 1\). By first-order Euler-Maclaurin,
Here \(\int _b^\infty \frac{dy}{y^s} = -\frac{b^{1-s}}{1-s}\) and \(d\left(\frac{1}{y^s}\right) = - \frac{s}{y^{s+1}} dy\). Hence, by \(\sum _{n\leq b} \frac{1}{n^s} = \zeta (s) - \sum _{n{\gt}b} \frac{1}{n^s}\) for \(\Re s {\gt} 1\),
Since the integral converges absolutely for \(\Re s {\gt} 0\), both sides extend holomorphically to \(\{ s\in \mathbb {C}: \Re s{\gt}0, s\ne 1\} \); thus, the equation holds throughout that region.
Let \(b{\gt}0\), \(b\in \mathbb {Z} + \frac{1}{2}\). Then, for all \(s\in \mathbb {C}\setminus \{ 1\} \) with \(\Re s {\gt} 0\),
Assume first that \(\Re s {\gt} 1\). By first-order Euler-Maclaurin and \(b\in \mathbb {Z}+\frac{1}{2}\),
Here \(\int _b^\infty \frac{dy}{y^s} = -\frac{b^{1-s}}{1-s}\) and \(d\left(\frac{1}{y^s}\right) = - \frac{s}{y^{s+1}} dy\). Hence, by \(\sum _{n\leq b} \frac{1}{n^s} = \zeta (s) - \sum _{n{\gt}b} \frac{1}{n^s}\) for \(\Re s {\gt} 1\),
Since the integral converges absolutely for \(\Re s {\gt} 0\), both sides extend holomorphically to \(\{ s\in \mathbb {C}: \Re s{\gt}0, s\ne 1\} \); thus, the equation holds throughout that region.
Let \(b{\gt}a{\gt}0\), \(b\in \mathbb {Z} + \frac{1}{2}\). Then, for all \(s\in \mathbb {C}\setminus \{ 1\} \) with \(\sigma = \Re s {\gt} 0\),
By Lemma 8.4.8, \(\sum _{n\leq a} = \sum _{n\leq b} - \sum _{a {\lt} n\leq b}\), \(\left|\{ y\} -\frac{1}{2}\right| \leq \frac{1}{2}\) and \(\int _b^\infty \frac{dy}{|y^{s+1}|} = \frac{1}{\sigma b^\sigma }\).
Let \(a,b\in \mathbb {R}\setminus \mathbb {Z}\), \(b{\gt}a{\gt}0\). Let \(s\in \mathbb {C}\setminus \{ 1\} \). Define \(f:\mathbb {R}\to \mathbb {C}\) by \(f(y) = 1_{[a,b]}(y)/y^s\). Then
Since \(a\notin \mathbb {Z}\), \(\sum _{a {\lt} n\leq b} \frac{1}{n^s} = \sum _{n\in \mathbb {Z}} f(n)\). By Poisson summation (as in [ 33 , Thm. D.3 ] )
where we use the facts that \(f\) is in \(L^1\), of bounded variation, and (by \(a,b\not\in \mathbb {Z}\)) continuous at every integer. Now
We could prove these equations starting from Euler’s product for \(\sin \pi z\).
Let \(z\in \mathbb {C}\), \(z\notin \mathbb {Z}\). Then
Let us start from the Mittag-Leffler expansion \(\pi \cot \pi s = \frac{1}{s} + \sum _n \left(\frac{1}{s-n} + \frac{1}{s+n}\right)\).
Applying the trigonometric identity \(\cot u - \cot \left(u + \frac{\pi }{2}\right) = \cot u + \tan u = \frac{2}{\sin 2 u}\) with \(u=\pi z/2\), and letting \(s = z/2\), \(s = (z+1)/2\), we see that
after reindexing the second sum. Regrouping terms again, we obtain our equation.
Let \(z\in \mathbb {C}\), \(z\notin \mathbb {Z}\). Then
Differentiate the expansion of \(\pi \cot \pi z\) term-by-term because it converges uniformly on compact subsets of \(\mathbb {C}\setminus \mathbb {Z}\). By \(\left(\pi \cot \pi z\right)' = - \frac{\pi ^2}{\sin ^2 \pi z}\) and \(\left(\frac{1}{z\pm n}\right)' = -\frac{1}{(z\pm n)^2}\), we are done.
For \(\vartheta \in \mathbb {R}\) with \(0\leq |\vartheta |{\lt} 1\),
Since \(\frac{1}{(n-\vartheta )^3} + \frac{1}{(n+\vartheta )^3}\) is even, we may replace \(\vartheta \) by \(|\vartheta |\). Then we rearrange the sum:
We may write \((n+1-|\vartheta |)^3\), \((n+|\vartheta |)^3\) as \((n+\frac{1}{2}-t)^3\), \((n+\frac{1}{2} + t)^3\) for \(t = |\vartheta |-1/2\). Since \(1/u^3\) is convex, \(\frac{1}{(n+1/2-t)^3} + \frac{1}{(n+1/2+t)^3}\) reaches its maximum on \([-1/2,1/2]\) at the endpoints. Hence
Let \(s = \sigma + i \tau \), \(\sigma \geq 0\), \(\tau \in \mathbb {R}\), with \(s\ne 1\). Let \(b{\gt}a{\gt}0\), \(a, b\in \mathbb {Z} + \frac{1}{2}\), with \(a{\gt}\frac{|\tau |}{2\pi }\). Define \(f:\mathbb {R}\to \mathbb {C}\) by \(f(y) = 1_{[a,b]}(y)/y^s\). Write \(\vartheta = \frac{\tau }{2\pi a}\), \(\vartheta _- = \frac{\tau }{2\pi b}\). Then
with absolute convergence, where \(g(t) = \frac{1}{\sin \pi t} - \frac{1}{\pi t}\) for \(t\ne 0\), \(g(0)=0\), and
By Proposition 8.4.1, multiplying by \(2\) (since \(e(-n t)+e(n t) = 2 \cos 2\pi n t\)),
where \(\vartheta _- = \tau /(2\pi b)\). Note \(|\vartheta _-|\leq |\vartheta |{\lt}1\). By the Lemma 8.4.11,
for \(z\ne 0\), while \(\sum _n \frac{(-1)^{n+1} 2 z}{n^2 - z^2} = \sum _n 0 = 0\) for \(z=0\). Moreover, by Lemmas 8.4.12 and 8.4.13, for \(\vartheta \ne 0\),
If \(\vartheta =0\), then \(\sum _n \left(\frac{\sigma }{(n-\vartheta )^2} + \frac{\sigma }{(n+\vartheta )^2}\right) = 2 \sigma \sum _{n=1}^\infty \frac{1}{n^2} = \sigma \frac{\pi ^2}{3}\).
Let \(s = \sigma + i \tau \), \(\sigma \geq 0\), \(\tau \in \mathbb {R}\), with \(s\ne 1\). Let \(a\in \mathbb {Z} + \frac{1}{2}\) with \(a{\gt}\frac{|\tau |}{2\pi }\). Then
where \(\vartheta = \frac{\tau }{2\pi a}\), \(c_\vartheta = \frac{i}{2} \left(\frac{1}{\sin \pi \vartheta } - \frac{1}{\pi \vartheta }\right)\) for \(\vartheta \ne 0\), \(c_0 =0\), and \(C_{\sigma ,\vartheta }\) is as in 4.
Assume first that \(\sigma {\gt}0\). Let \(b\in \mathbb {Z}+\frac{1}{2}\) with \(b{\gt}a\), and define \(f(y) = \frac{1_{[a,b]}(y)}{y^s}\). By Lemma 8.4.9 and Lemma 8.4.10,
We apply Lemma 8.4.14 to estimate \(\lim _{N\to \infty } \sum _{n=1}^N (\widehat{f}(n) + \widehat{f}(-n))\). We obtain
where \(\vartheta _- = \frac{\tau }{2\pi b}\) and \(g(t)\) is as in Lemma 8.4.14, and so \(-\frac{g(\vartheta )}{2 i} = c_\vartheta \). We let \(b\to \infty \) through the half-integers, and obtain 8, since \(b^{-\sigma }\to 0\), \(\vartheta _-\to 0\) and \(g(\vartheta _-)\to g(0) = 0\) as \(b\to \infty \).
Finally, the case \(\sigma =0\) follows since all terms in 8 extend continuously to \(\sigma =0\).
The term \(c_\vartheta a^{-s}\) in 8 does not seem to have been worked out before in the literature; the factor of \(i\) in \(c_\vartheta \) was a surprise. For the sake of comparison, let us note that, if \(a\geq x\), then \(|\vartheta |\leq 1/2\pi \), and so \(|c_\vartheta |\leq |c_{\pm 1/2\pi }| = 0.04291\dotsc \) and \(|C_{\sigma ,\vartheta }|\leq |C_{\sigma ,\pm 1/2\pi }|\leq 0.176\sigma +0.246\). While \(c_\vartheta \) is optimal, \(C_{\sigma ,\vartheta }\) need not be – but then that is irrelevant for most applications.
8.5 An explicit zero-free region for \(\zeta \)
In this section we begin a formalisation of the zero-free region for the Riemann zeta function of Kadiri [ 28 ] , who proved that \(\zeta (s)\) has no zeros in the region
The initial target is the explicit formula [ 28 , (5) ] for \(\Re \sum _{n \geq 1} \frac{\Lambda (n)}{n^s} f(\log n)\) expressed as a sum over the non-trivial zeros of \(\zeta \), where \(f\) is a suitable smooth, compactly supported test function and \(s\) a complex parameter.
The constant \(B \in \mathbb {C}\) appearing in the Hadamard product factorisation of the Riemann zeta function:
Concretely \(B = -\tfrac {\gamma }{2} - 1 + \tfrac {1}{2} \log (4\pi )\) in terms of the Euler-Mascheroni constant \(\gamma \) ( [ ). For our purposes it appears only as the additive constant in 8.5.1, and the identity \(\Re B = -\sum _{\rho \in Z(\zeta )} \Re \tfrac {1}{\rho }\) used in the derivation of 8.5.1.
For every \(s \in \mathbb {C}\) that is neither \(1\) nor a non-trivial zero of \(\zeta \),
where \(B\) is the Hadamard constant (8.5.1). This is the logarithmic derivative of the Hadamard factorisation of \(\zeta \) ( [ ).
Differentiate the Hadamard product (8.5.1) logarithmically; the linear-in-\(s\) term in the exponential collapses to the constant \(B\). The \(\tfrac {1}{s-1}\) term comes from the \((s-1)\zeta (s)\) prefactor and the \(\tfrac {1}{2} \Gamma '/\Gamma \) term from the gamma factor. To be formalised.
Let \(\varphi \colon \mathbb {R} \to \mathbb {C}\) be \(C^1\) and suppose there exists \(b {\gt} 0\) such that both \(\varphi (x) e^{x/2}\) and \(\varphi '(x) e^{x/2}\) are \(O(e^{-(1/2 + b)|x|})\) as \(|x| \to \infty \). Define the Laplace transform \(\Phi (z) := \int _0^{\infty } \varphi (y) e^{-zy}\, dy\). Then
where the \(\rho \)-sum runs over the non-trivial zeros of \(\zeta \).
This is the \(q = 1\), \(\chi \) trivial case of the Weil-type explicit formula of [ 28 , Theorem 3.1 ] . The \(\Phi (-1)\) term comes from the simple pole of \(\zeta \) at \(z = 1\) (and is absent for non-trivial \(\chi \)); the \(\varphi (0)\log \pi \) term and the \(\Gamma \)-integral come from the gamma factor in the functional equation of \(\zeta \); the \(\sum _n \tfrac {\Lambda (n)}{n}\varphi (-\log n)\) term is the contribution from the reflected (\(z \leftrightarrow 1 - z\)) Dirichlet series.
Classical Weil-style argument. Write the LHS as a Mellin contour integral \(\tfrac {1}{2\pi i} \int _{(c)} (-\zeta '/\zeta )(z)\, \Phi (-z)\, dz\) for some \(c {\gt} 1\), using the Dirichlet series \(-\zeta '/\zeta (z) = \sum _n \Lambda (n) n^{-z}\) on \(\Re z {\gt} 1\) together with the Mellin inversion \(\varphi (\log n) = \tfrac {1}{2\pi i} \int _{(c)} n^z \Phi (-z)\, dz\). Contour-shift to \(\Re z = -1 - a\) for some \(0 {\lt} a {\lt} b\), picking up residues at: \(z = 1\) (the simple pole of \(\zeta \), contributing \(\Phi (-1)\)); \(z = 0\) (contributing \(\Phi (0)\) via the Laurent expansion of \(-\zeta '/\zeta \) at \(0\)); and each non-trivial zero \(z = \rho \) (contributing \(-\Phi (-\rho )\)). Then use the functional equation \(\zeta (z) \Gamma (z/2) \pi ^{-z/2} = \zeta (1-z) \Gamma ((1-z)/2) \pi ^{-(1-z)/2}\) to rewrite the integral on \(\Re z = -1 - a\) as the reflected Dirichlet series \(\sum _n \tfrac {\Lambda (n)}{n} \varphi (-\log n)\) plus the \(\Gamma '/\Gamma \) contour integral on \(\Re z = 1/2\), with the \(\pi ^{z/2}\) factor producing \(-\varphi (0)\log \pi \). To be formalised.
For \(f\) satisfying the hypotheses \((H_1)\) of 8.5.1: for every \(w \in \mathbb {C}\) with \(w \neq 0\),
where \(F_2(w) := \int _0^d e^{-wy} f''(y)\, dy\) is the Laplace transform of \(f''\).
Two successive integrations by parts on \(F(w) = \int _0^d e^{-wy} f(y)\, dy\). The first gives \(F(w) = \tfrac {f(0)}{w} - \tfrac {f(d) e^{-w d}}{w} + \tfrac {1}{w} \int _0^d e^{-wy} f'(y)\, dy\); using \(f(d) = 0\) from \((H_1)\) kills the boundary term, leaving \(\tfrac {f(0)}{w} + \tfrac {1}{w} \int _0^d e^{-wy} f'(y)\, dy\). The second IBP on the remaining integral gives \(\tfrac {1}{w} \int _0^d e^{-wy} f'(y)\, dy = \tfrac {f’(0)}{w^2} - \tfrac {f’(d) e^{-w d}}{w^2} + \tfrac {1}{w^2} \int _0^d e^{-wy} f''(y)\, dy\); using \(f'(0) = f'(d) = 0\) from \((H_1)\) kills both boundary terms, leaving \(F_2(w)/w^2\). To be formalised.
The function \(\varphi (\cdot ;\, s)\) is smooth on each of the three open pieces: on \((-\infty , 0)\) it is \(\equiv 0\); on \((0, d)\) it equals \((f(0) - f(y)) e^{-sy}\), \(C^2\) from \(f \in C^2\) on \([0, d]\); on \((d, \infty )\) it equals \(f(0) e^{-sy}\) (using \(\mathrm{supp}\, f \subseteq [0, d)\)), smooth. At the seam \(y = 0\): the right-limits of \(\varphi \) and \(\varphi '\) are \((f(0) - f(0)) \cdot 1 = 0\) and \(-f'(0) - s(f(0) - f(0)) = 0\) respectively (using \(f'(0) = 0\) from \((H_1)\)), matching the left-limits \(0\). At the seam \(y = d\): the left-limits of \(\varphi \) and \(\varphi '\) are \((f(0) - f(d)) e^{-sd} = f(0) e^{-sd}\) (using \(f(d) = 0\)) and \(-f'(d) e^{-sd} - s(f(0) - f(d)) e^{-sd} = -s f(0) e^{-sd}\) (using \(f(d) = f'(d) = 0\)), matching the right-limits. Hence \(\varphi \) is \(C^1\) globally. To be formalised.
For \(f\) satisfying \((H_1)\) of 8.5.1 and \(s \in \mathbb {C}\) with \(\Re s {\gt} 1\), the Kadiri test function \(\varphi \) satisfies decay condition (B) of 8.5.1: there exists \(b {\gt} 0\) (any \(0 {\lt} b {\lt} \Re s - 1\) works) such that both \(\varphi (x;\, s) e^{x/2}\) and \(\varphi '(x;\, s) e^{x/2}\) are \(O(e^{-(1/2 + b)|x|})\) as \(|x| \to \infty \).
For \(x {\lt} 0\) both \(\varphi (x;\, s)\) and \(\varphi '(x;\, s)\) are identically \(0\), so the bound holds trivially at \(-\infty \). For \(x {\gt} d\) (above the support of \(f\)), \(\varphi (x;\, s) = f(0)\, e^{-x s}\) and \(\varphi '(x;\, s) = -s\, f(0)\, e^{-x s}\), so \(|\varphi (x;\, s) e^{x/2}| = |f(0)|\, e^{-x(\Re s - 1/2)}\) and similarly for the derivative with an extra factor \(|s|\); both are \(O(e^{-(1/2 + b) x})\) as \(x \to +\infty \) precisely when \(\Re s - 1/2 \geq 1/2 + b\), i.e. \(b \leq \Re s - 1\). Take any \(0 {\lt} b {\lt} \Re s - 1\). To be formalised.
For \(f\) satisfying \((H_1)\) of 8.5.1 and \(s, z \in \mathbb {C}\) with \(\Re (s + z) {\gt} 0\),
where \(F\) is the Laplace transform of \(f\).
Direct expansion of the integrand on \(y {\gt} 0\): \(\varphi (y;\, s) e^{-zy} = (f(0) - f(y)) e^{-(s+z) y}\). Split the integral: \(\int _0^{\infty } f(0)\, e^{-(s+z) y}\, dy = f(0)/(s + z)\) converges by \(\Re (s + z) {\gt} 0\); \(\int _0^{\infty } f(y)\, e^{-(s+z) y}\, dy = F(s + z)\) unconditionally since \(\mathrm{supp}\, f \subseteq [0, d]\) makes the integral compactly-supported. To be formalised.
\(\Re B = -\sum _{\rho \in Z(\zeta )} \Re \tfrac {1}{\rho }\), where \(B\) is the Hadamard constant (8.5.1).
Subtract \(\tfrac {1}{s-1}\) from 8.5.1, take \(s \to 1\) using the Laurent expansion \(-\zeta '/\zeta (s) = \tfrac {1}{s-1} - \gamma + O(s - 1)\) near \(s = 1\) and the value \(\Gamma '/\Gamma (3/2)\), then symmetrise the resulting sum \(\sum _\rho (1/\rho + 1/(1-\rho ))\) using \(\rho \leftrightarrow 1 - \bar\rho \) to relate \(\sum _\rho 1/\rho \) to \(\Re B\). To be formalised.
Backlund’s explicit zero-counting bound ( [ 2 ] , cited in [ 28 , page 24 ] ): the constants \((b_1, b_2, b_3) = (0.137, 0.443, 6.1)\) satisfy the project’s 8.1.5, i.e. for every \(T \geq 2\),
Backlund’s original ( [ 28 , page 24 ] ) bounds the difference from the simpler main term \(\tfrac {T}{2\pi } \log \tfrac {T}{2\pi e}\) by \(0.137 \log T + 0.443 \log \log T + 5.225\); absorbing the \(\tfrac {7}{8}\) offset between the two main-term conventions gives the project-form constant \(5.225 + \tfrac {7}{8} = 6.1\). For \(T \in [2, t_1)\) (below the first non-trivial zero \(t_1 \approx 14.1347\)) the LHS reduces to the main-term absolute value, which is well within the (loose) RHS bound.
Under the hypotheses of 8.5.1: for every closed vertical strip \(\sigma _0 \leq \Re s \leq \sigma _1\) there is a constant \(C = C(\sigma _0, \sigma _1, f)\) such that for every \(s \in \mathbb {C}\) with \(\sigma _0 \leq \Re s \leq \sigma _1\) and \(|\Im s| \geq 1\),
Note that this is sharper than the elementary \(|F(s)| = O(1/|s|)\) from a single integration by parts: the cancellation \(\Re (1/s) = \sigma /(\sigma ^2 + y^2) = O(1/y^2)\) for bounded \(\sigma \) saves one power of \(|y|\) once the real part is taken.
Apply 8.5.2 to get \(F(s) = f(0)/s + F_2(s)/s^2\), where \(F_2\) is the Laplace transform of \(f''\). Taking real parts at \(s = \sigma + iy\): \(\Re F(s) = \dfrac {f(0)\, \sigma }{\sigma ^2 + y^2} + \Re \dfrac {F_2(s)}{s^2}\). The first summand is bounded by \(|f(0)| \cdot \max (|\sigma _0|, |\sigma _1|) / y^2\); the second by absolute values is at most \(\dfrac {1}{y^2} \cdot d \cdot \max (1, e^{-\sigma _0 d}) \cdot \| f''\| _\infty \) (using \(\mathrm{supp}\, f'' \subseteq [0, d]\)). Both depend only on \(\sigma _0, \sigma _1, d, f\); take \(C\) to be their sum. To be formalised.
Under the hypotheses of 8.5.1, the sum \(\sum _{\rho \in Z(\zeta )} \Re F(s - \rho )\) over the non-trivial zeros of \(\zeta \) is convergent (Lean: ‘Summable‘).
Combine 8.5.8 (giving \(|\Re F(s-\rho )| \leq C/|\Im (s-\rho )|^2 = C/(\Im s - \gamma )^2\) for \(|\gamma |\) large, since the real part \(\Re (s-\rho ) = \Re s - \beta \) stays in the bounded strip \([\Re s - 1, \Re s]\)) with the unconditional crude counting bound \(N(T) = O(T^{3/2})\) proved in the Backlund zero-count module: over the dyadic shells \(|\gamma | \in [2^k, 2^{k+1})\) the shell count is \(O(3^k)\) while each term is at most \(4^{-k}\), so \(\sum _{|\gamma | \geq 1} 1/|\gamma |^2 {\lt} \infty \). The finitely many small-\(|\gamma |\) terms are absorbed by cofiniteness. The sharper 8.5.7 route (\(N(T) \ll T \log T\)) is not needed here and remains the path to the explicit numerics.
Under the hypotheses of 8.5.1: for every \(s \in \mathbb {C}\) with \(\Re s {\gt} 1\),
The zero sum is grouped: each summand is \(\Phi (-\rho )\), the Laplace transform of the test function \(\varphi (y) = (f(0) - f(y)) e^{-y s}\) at \(-\rho \), equal to \(-F_2(s-\rho )/(s-\rho )^2\) and hence of size \(O(1/|\Im \rho |^2)\); the split sums \(\sum _\rho 1/(s-\rho )\) and \(\sum _\rho F(s-\rho )\) are individually divergent.
Apply 8.5.1 to the Kadiri test function \(\varphi \); its hypotheses are discharged by 8.5.3 (\(\varphi \) is \(C^1\)) and 8.5.4 (decay (B) with any \(0 {\lt} b {\lt} \Re s - 1\), requiring \(\Re s {\gt} 1\)). The Laplace transform of \(\varphi \) is computed by 8.5.5: \(\Phi (z;\, s) = f(0)/(s+z) - F(s+z)\). In particular \(\Phi (-1) = f(0)/(s-1) - F(s-1)\), \(\Phi (-\rho ) = f(0)/(s-\rho ) - F(s-\rho )\), \(\Phi (0) = f(0)/s - F(s)\), and \(\Phi (-z) = f(0)/(s-z) - F(s-z)\) at \(z = 1/2 + it\). Rewriting \(F(s) = f(0)/s + F_2(s)/s^2\) via 8.5.2 (and likewise at \(w = s - z\)) collapses \(\Phi (0) = -F_2(s)/s^2\) and \(\Phi (-z) = -F_2(s-z)/(s-z)^2\) used inside the contour integral. Three terms of 8.5.1’s conclusion vanish for this \(\varphi \): \(\varphi (0;\, s) = 0\) kills the \(\varphi (0) \log \pi \) term, and \(\varphi (-\log n;\, s) = 0\) for every \(n \geq 1\) kills the reflected discrete sum. Unfolding \(\varphi (\log n;\, s) = (f(0) - f(\log n))/n^s\) gives \(\sum _n \Lambda (n) \varphi (\log n;\, s) = f(0) \sum _n \Lambda (n)/n^s - \sum _n \Lambda (n) f(\log n)/n^s\); solving for \(\sum _n \Lambda (n) f(\log n)/n^s\) and substituting the \(\Phi \) values yields the right-hand side.
Under the hypotheses of 8.5.1: for every \(s \in \mathbb {C}\) with \(\Re s {\gt} 1\),
This is the real-part form of 8.5.1; the substantive derivation from 8.5.1 via the Kadiri test function \(\varphi (y) = (f(0) - f(y)) e^{-y s} \mathbf{1}_{y \geq 0}\) lives in that sublemma. The zero contribution in the \(f(0)\)-coefficient uses the absolutely convergent Hadamard-paired block \(\sum _\rho (1/\rho + 1/(s - \rho ))\) together with the absolutely convergent real correction \(\sum _\rho \Re (1/\rho )\), matching 8.5.1; the standalone \(\sum _\rho 1/(s - \rho )\) does not converge unconditionally. The restriction \(\Re s {\gt} 1\) is where the Dirichlet series for \(-\zeta '/\zeta (s)\) converges absolutely; this is also the range used in Kadiri’s downstream zero-free region argument, so we do not extend further.
Apply 8.5.1 to obtain the \(\mathbb {C}\)-valued equation, then take real parts of both sides. The grouped zero sum is absolutely summable (each summand is \(-F_2(s-\rho )/(s-\rho )^2\) by 8.5.2), so \(\Re \) passes through it; each term splits as \(f(0) \Re (1/(s-\rho )) - \Re F(s-\rho )\), and both real families are absolutely summable. Regrouping \(\sum _\rho \Re (1/(s-\rho ))\) into the paired block minus the \(\Re (1/\rho )\) correction is legitimate by the paired-family summability.
For every \(s \in \mathbb {C}\) with \(\Re s {\gt} 1\),
The zero block is the absolutely convergent Hadamard pairing of 8.5.1, and the \(\Re (1/\rho )\) correction is absolutely convergent; the standalone \(\sum _\rho 1/(s - \rho )\) does not converge unconditionally. This is the identity that turns the \(f(0)\)-coefficient of equation (16) into the \(T_1\) form of 8.5.1.
For \(\Re s {\gt} 1\) the Dirichlet series gives \(\sum \Lambda (n)/n^s = -\zeta '/\zeta (s)\); substitute 8.5.1 (treating the equation as one in \(\mathbb {C}\), not yet taking \(\Re \)). The \(1/(s-1)\) terms and the paired zero blocks cancel exactly, leaving \(-B - \tfrac {1}{2}\log \pi + \tfrac {1}{2}\Gamma '/\Gamma (s/2+1)\). Taking real parts and applying 8.5.6 cancels \(\Re B\) against the \(\sum _\rho \Re (1/\rho )\) correction, leaving the claim.
Let \(d {\gt} 0\) and let \(f \colon [0, d] \to \mathbb {R}\) be a non-negative function of class \(C^2\) on \([0, d]\), compactly supported in \([0, d)\), satisfying the boundary conditions \(f(d) = f'(0) = f'(d) = f''(d) = 0\) (hypothesis \((H_1)\) of [ 28 ] ). Let \(F\) denote its Laplace transform \(F(s) = \int _0^d e^{-s t} f(t)\, dt\), and let \(F_2\) denote the Laplace transform of \(f''\). Then for every \(s \in \mathbb {C}\) with \(\Re s {\gt} 1\), the sum \(\sum _{\rho \in Z(\zeta )} \Re F(s - \rho )\) over the non-trivial zeros is convergent, and
where \(Z(\zeta )\) is the set of non-trivial zeros of \(\zeta \) (those in the open critical strip \(0 {\lt} \Re \rho {\lt} 1\)). The half-plane \(\Re s {\gt} 1\) is the range used in Kadiri’s downstream zero-free region argument; the harmonic-extension step that would lift the identity to all of \(\mathbb {C}\) is not needed for that application.
For \(f\) as in 8.5.1, real parameters \(\kappa , \delta \), and \(s \in \mathbb {C}\), set
where \(T_1, T_2\) are the "gamma" and "remainder" contributions to the RHS of 8.5.1. Then
Direct substitution: apply 8.5.1 at \(s\) and at \(s + \delta \), multiply the latter by \(\kappa \), subtract, and use the identity \(n^{-s} - \kappa n^{-(s + \delta )} = n^{-s} (1 - \kappa n^{-\delta })\) to combine the LHS, while the definitions of \(\Delta _1, \Delta _2, D\) combine the corresponding RHS terms.