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

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)|\).

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 \(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\).

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,

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}\),

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\).

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.

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.

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

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 [ 32 , 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

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.

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.

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

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

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\).

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.

Standard inverse-Laplace theorem (e.g. Widder, The Laplace Transform, Ch. III, Theorem 7.3). Hypotheses (A) (regularity / mean-value condition at jumps) and (B) (the \(O(1/|t|)\) decay of \(\Phi \) on the strip) provide exactly what is needed for the inversion integral to converge absolutely and recover \(\varphi \) at \(y = \log n \geq 0\). To be formalised.

Corollary of 8.5.1: multiply that identity by \(\Lambda (n)\), sum over \(n \geq 1\), and exchange sum and integral (justified by absolute convergence of the Dirichlet series for \(-\zeta '/\zeta \) on \(\sigma {\gt} 1\) combined with the \(O(1/|t|)\) decay of \(\Phi \) from (B)). The Dirichlet series identity \(-\zeta '/\zeta (s) = \sum _n \Lambda (n) n^{-s}\) converts the sum into a factor of \(-\zeta '/\zeta (s)\) in the integrand. Finally, change of variable \(s \mapsto -s\) maps the contour \(\sigma = -(1 + a)\) to \(\sigma = 1 + a\) (with the orientation-flip cancelling the sign from \(ds\)). To be formalised.

Apply the residue theorem to \((-\zeta '/\zeta )(s) \Phi (-s)\) on the counterclockwise rectangle with vertices \(1+a-iT\), \(1+a+iT\), \(-a+iT\), \(-a-iT\). Between \(\sigma = -a\) and \(\sigma = 1+a\), the integrand has poles only at \(s = 1\) (a simple pole of \(-\zeta '/\zeta \) with residue \(+\Phi (-1)\), from the simple pole of \(\zeta \) at \(s = 1\)) and at each non-trivial zero \(s = \rho \in Z(\zeta )\) with \(|\Im \rho | {\lt} T\) (a pole of \(-\zeta '/\zeta \) with residue \(-\mathrm{ord}_\zeta (\rho )\, \Phi (-\rho )\), weighted by the multiplicity of \(\rho \)). [Note: \(\zeta (0) = -1/2 \neq 0\), so there is no pole at \(s = 0\); the trivial zeros at \(s = -2, -4, \ldots \) all lie to the left of \(\sigma = -a\) and are not enclosed.] To be formalised.

The integrand has \(|\Phi (-s)| = O(1/|t|) = O(1/T)\) on the horizontal arc (by (B), uniformly on the closed strip \(-a \leq \sigma \leq 1 + a\)), and \(-\zeta '/\zeta (s)\) grows at most polynomially in \(\log |\Im s| = \log T\) on this strip. The horizontal arc has fixed length \(1 + 2a\), so the integral is bounded by \(O((\log T)^k / T) \to 0\) as \(T \to \infty \). To be formalised.

Identical argument to 8.5.4, with \(T\) replaced by \(-T\) (the decay bound on \(\Phi \) is symmetric in \(t\), and the growth bound on \(-\zeta '/\zeta \) depends only on \(|t|\)). To be formalised.

Take the logarithmic derivative of the completed-zeta functional equation \(\zeta (s)\, \Gamma (s/2)\, \pi ^{-s/2} = \zeta (1-s)\, \Gamma ((1-s)/2)\, \pi ^{-(1-s)/2}\) (with appropriate \((s-1)\) regularization at \(s = 1\)). Differentiating both sides with respect to \(s\) gives \(\zeta '/\zeta (s) + \tfrac {1}{2}\Gamma '/\Gamma (s/2) - \tfrac {1}{2}\log \pi = -\zeta '/\zeta (1-s) - \tfrac {1}{2}\Gamma '/\Gamma ((1-s)/2) + \tfrac {1}{2}\log \pi \), and solving for \(-\zeta '/\zeta (s)\) yields the stated identity (note the chain-rule sign from \(d(1-s)/ds = -1\) giving the \(+\zeta '/\zeta (1-s)\) term). To be formalised.

Apply 8.5.6 pointwise inside the integral. The hypotheses of the functional equation hold on the entire contour \(\sigma = -a\): \(s = -a + it \neq 1\) (since \(\Re s = -a \leq 0\)), \(s \neq 0\) (since \(a {\gt} 0\)), \(s \notin Z(\zeta )\) (since \(\Re s = -a {\lt} 0\) but non-trivial zeros have \(\Re \rho \in (0, 1)\)), and \(1 - s \notin Z(\zeta )\) (since \(\Re (1 - s) = 1 + a {\gt} 1\)). Linearity of the integral splits it into the three pieces of the definitions of \(I_1, I_2, I_3\). To be formalised.

The constant prefactor \(\log (1/\pi )\) pulls out of the integral. The remaining \(\tfrac {1}{2\pi i} \int _{-a - iT}^{-a + iT} \Phi (-s)\, ds\) tends to \(\varphi (0)\) as \(T \to \infty \) by the Laplace-inversion identity at \(y = 0\) (8.5.1 specialized to \(n = 1\), with a change of variable \(s \mapsto -s\) that maps the \(\sigma = -a\) contour back to \(\sigma = a\)). To be formalised.

On the contour \(\sigma = -a\), write \(1 - s = (1 + a) - i\Im s\) so \(\Re (1 - s) = 1 + a {\gt} 1\), and use the Dirichlet series \(\zeta '/\zeta (1-s) = -\sum _n \Lambda (n) n^{-(1-s)}\) (von Mangoldt with a leading minus). The integrand \(\zeta '/\zeta (1-s)\, \Phi (-s)\) thus expands as \(-\sum _n \Lambda (n) n^{-(1-s)} \Phi (-s)\). Exchange sum and integral (justified by absolute convergence and the \(O(1/|t|)\) decay of \(\Phi \)); apply 8.5.1 at \(y = -\log n\) to identify the inner integral as \(n^a \varphi (-\log n)\), and combine with the \(n^{-(1+a)}\) from the Dirichlet series and the overall minus to get \(-\sum _n (\Lambda (n)/n)\, \varphi (-\log n)\). To be formalised.

On \(\Re s = 1/2\), \(1 - s = \bar s\), hence \((1 - s)/2 = \overline{s/2}\). Since \(\Gamma '/\Gamma \) has real Taylor coefficients away from its poles, it commutes with complex conjugation: \(\Gamma '/\Gamma ((1-s)/2) = \overline{\Gamma '/\Gamma (s/2)}\). Then \(\tfrac {1}{2}(z + \bar z) = \Re z\) with \(z = \Gamma '/\Gamma (s/2)\). To be formalised.

Shift the contour of \(I_3(T)\) from \(\sigma = -a\) to \(\sigma = 1/2\). The integrand \(\tfrac {1}{2}\{ \Gamma '/\Gamma (s/2) + \Gamma '/\Gamma ((1-s)/2)\} \, \Phi (-s)\) has a simple pole at \(s = 0\) from \(\Gamma '/\Gamma (s/2) \sim -2/s\) near \(s = 0\), with residue \(+\Phi (0)\) contributed by the leftward shift; no other poles lie in \(-a {\lt} \Re s {\lt} 1/2\). The horizontal arcs vanish as \(T \to \infty \) by (B). On \(\Re s = 1/2\), apply 8.5.10 to identify the integrand as \(\Re [\Gamma '/\Gamma (s/2)]\, \Phi (-s)\). The Bochner integral in the limit value is well-defined precisely under the explicit integrability hypothesis on the \(\Gamma \)-contour integrand (otherwise the integral evaluates to \(0\) by Mathlib’s convention and the statement is vacuous); this same hypothesis is carried by 8.5.1. To be formalised.

Composition of the eleven preceding sublemmas. Pick any \(0 {\lt} a {\lt} \min (b, 1)\) and any \(T {\gt} 0\).

By 8.5.2 the LHS equals \(\tfrac {1}{2\pi i} \int _{(1+a)} (-\zeta '/\zeta )(s)\, \Phi (-s)\, ds\), which is the \(T \to \infty \) limit of 8.5.2’s \(I(T)\) by dominated convergence on the \(O(1/|t|)\) decay of \(\Phi \).

By 8.5.3 this \(I(T)\) equals the sum of the \(\sigma = -a\) integral, the two horizontal arcs, \(\Phi (-1)\), and the truncated \(\rho \)-sum \(\sum _{|\Im \rho | {\lt} T} \Phi (-\rho )\). The two horizontals vanish in the limit by 8.5.4 and 8.5.5, while the truncated \(\rho \)-sum extends to the full \(\sum _{\rho \in Z(\zeta )} \Phi (-\rho )\) as \(T \to \infty \) (using summability of the complex sum).

The \(\sigma = -a\) integral equals \(I_1(T) + I_2(T) + I_3(T)\) by 8.5.7, with \(T \to \infty \) limits given by 8.5.8 (\(\to -\varphi (0) \log \pi \)), 8.5.9 (\(\to -\sum _n \tfrac {\Lambda (n)}{n}\varphi (-\log n)\)), and 8.5.11 (\(\to \Phi (0) + \tfrac {1}{2\pi i} \int _{(1/2)} \Re [\Gamma '/\Gamma (s/2)]\, \Phi (-s)\, ds\)).

Combining yields the stated identity. The residual ‘sorry‘ covers the remaining technical limit-management steps (interchange of \(T \to \infty \) with the integrals and the \(\rho \)-sum); the sublemma signatures already type-check the composition.

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 \(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.

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.

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.

Classical Backlund 1918 ( [ 2 ] ). The [ 2 , Theorem of Backlund ] variant is the form cited at [ 27 , page 24 ] as the starting point for the explicit estimates \(N_1(u), N_2(u)\) of (34)-(35) there. To be formalised.

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.

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.

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.

Apply 8.5.12 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 \(\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.

The ‘Summable‘ conjunct is 8.5.9. For the identity, combine 8.5.10 (the (16)-form on \(\Re s {\gt} 1\)) with 8.5.11 (which substitutes the \(T_1\) form for the \(f(0)\)-coefficient \(\Re \)-expression, also on \(\Re s {\gt} 1\)). The result is a two-line ‘rw‘ chain.

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.