This is the Riemann Removable Singularity Theorem, slightly rephrased from what’s in Mathlib. (We don’t care what the function \(g\) is, just that it’s holomorphic.)

This is in a Mathlib PR.

Chop the big rectangle with two vertical cuts and two horizontal cuts into smaller rectangles, the middle one being the desired square. The integral over each of the outer rectangles vanishes, since \(f\) is holomorphic there. (The constant \(c\) being “small enough” here just means that the inner square is strictly contained in the big rectangle.)

This is a special case of the more general result above.

Replace \(f\) with \(g + A/(s-p)\) in the integral. The integral of \(g\) vanishes by Lemma 4. To evaluate the integral of \(1/(s-p)\), pull everything to a square about the origin using Lemma 18, and rescale by \(c\); what remains is handled by Lemma 19.

Standard.

Standard.

Composition of differentiabilities.

This integral is between \(\frac{1}{2}\) and \(1\) of the integral of \(\frac{1}{1+t^2}\), which is \(\pi \).

Triangle inequality and pointwise estimate.

Triangle inequality and pointwise estimate.

By 25, \(f\) is continuous, so it is integrable on any interval.

Also, \(|f(x)| = \Theta (x^{-2})\) as \(x\to \infty \),

and \(|f(-x)| = \Theta (x^{-2})\) as \(x\to \infty \).

Since \(g(x) = x^{-2}\) is integrable on \([a,\infty )\) for any \(a{\gt}0\), we conclude.

The numerator is bounded and the denominator tends to infinity.

The numerator is bounded and the denominator tends to infinity.

Let \(f(s) = x^s/(s(s+1))\). Then \(f\) is holomorphic on the half-plane \(\{ s\in \mathbb {C}:\Re (s){\gt}0\} \). The rectangle integral of \(f\) with corners \(\sigma -iT\) and \(\sigma +iT\) is zero. The limit of this rectangle integral as \(T\to \infty \) is \(\int _{(\sigma ')}-\int _{(\sigma )}\). Therefore, \(\int _{(\sigma ')}=\int _{(\sigma )}\).

But we also have the bound \(\int _{(\sigma ')} \leq x^{\sigma '} * C\), where

\(C=\int _\mathbb {R}\frac{1}{|(1+t)(1+t+1)|}dt\).

Therefore \(\int _{(\sigma ')}\to 0\) as \(\sigma '\to \infty \).

By ring.

Applying Lemma 33, the function \(s ↦ x^s/s(s+1) - 1/s = x^s/s - x^0/s - x^s/(1+s)\). The last term is bounded for \(s\) away from \(-1\). The first two terms are the difference quotient of the function \(s ↦ x^s\) at \(0\); since it’s differentiable, the difference remains bounded as \(s\to 0\).

Applying Lemma 33, the function \(s ↦ x^s/s(s+1) - x^{-1}/(s+1) = x^s/s - x^s/(s+1) - (-x^{-1})/(s+1)\). The first term is bounded for \(s\) away from \(0\). The last two terms are the difference quotient of the function \(s ↦ x^s\) at \(-1\); since it’s differentiable, the difference remains bounded as \(s\to -1\).

For \(c{\gt}0\) sufficiently small,

\(x^s/(s(s+1))\) is equal to \(1/s\) plus a function, \(g\), say, holomorphic in the whole rectangle (by Lemma 34).

Now apply Lemma 20.

Compute the integral.

We pull to a square with corners at \(-c-i*c\) and \(c+i*c\) for \(c{\gt}0\) sufficiently small. By Lemma 36, the integral over this square is equal to \(1\).

Pull contour from \((-1/2)\) to \((-3/2)\).

Pull contour from \((-3/2)\) to \((\sigma )\).

Let \(f(s) = x^s/(s(s+1))\). Then \(f\) is holomorphic on \(\mathbb {C}\setminus {0,-1}\).

First pull the contour from \((\sigma )\) to \((-1/2)\), picking up a residue \(1\) at \(s=0\).

Next pull the contour from \((-1/2)\) to \((-3/2)\), picking up a residue \(-1/x\) at \(s=-1\).

Then pull the contour all the way to \((\sigma ')\) with \(\sigma '{\lt}-3/2\).

For \(\sigma ' {\lt} -3/2\), the integral is bounded by \(x^{\sigma '}\int _\mathbb {R}\frac{1}{|(1+t ^2)(2+t ^2)|^{1/2}}dt\).

Therefore \(\int _{(\sigma ')}\to 0\) as \(\sigma '\to \infty \).

Partial integration.

This is a straightforward calculation.

This is a straightforward calculation.

The proof is from [Goldfeld-Kontorovich 2012]. Integrate by parts twice (assuming \(f\) is twice differentiable, and all occurring integrals converge absolutely, and boundary terms vanish).

We now have at least quadratic decay in \(s\) of the Mellin transform. Inserting this formula into the inversion formula and Fubini-Tonelli (we now have absolute convergence!) gives:

Apply the Perron formula to the inside:

where we integrated by parts (undoing the first partial integration), and finally applied the fundamental theorem of calculus (undoing the second).

By Definition 6,

in which we change variables to \(z=x/y\):

By Definitions 4 and 6

By (??) and Fubini’s theorem,

in which we change variables from \(x\) to \(z=x/y\):

which, by Definition 4, is

Same idea as Urysohn-type argument.

Integrate by parts:

Since \(\Re (s)\) is bounded, the right-hand side is bounded by a constant times \(1/|s|\).

Substitute \(y=x^{1/\epsilon }\), and use the fact that \(\nu \) has mass one, and that \(dx/x\) is Haar measure.

Substitute \(y=x^{1/\epsilon }\), use Haar measure; direct calculation.

This is immediate from the above theorem.

By Lemma 7,

which by Definition 4 is

Since \(\nu (x) x^{\epsilon -1}\) is integrable (because \(\nu \) is continuous and compactly supported),

By Taylor’s theorem,

so, since \(\nu \) is absolutely integrable,

We conclude the proof using Theorem 7.

This is a straightforward calculation.

Let \(c:=2^\epsilon {\gt} 1\), in terms of which we wish to prove

Letting \(f(x):=x\log x - x\), we can rewrite this as \(f(1) {\lt} f(c)\). Since

\(f\) is monotone increasing on [1, ∞), and we are done.

Opening the definition, we have that the Mellin convolution of \(1_{(0,1]}\) with \(\nu _\epsilon \) is

The support of \(\nu _\epsilon \) is contained in \([1/2^\epsilon ,2^\epsilon ]\), so it suffices to consider \(y \in [1/2^\epsilon x,2^\epsilon x]\) for nonzero contributions. If \(x {\lt} 2^{-\epsilon }\), then the integral is the same as that over \((0,\infty )\):

in which we change variables to \(z=x/y\) (using \(x{\gt}0\)):

which is equal to one by Lemma 46. We then choose

which satisfies

by Lemma ??, so

Again the Mellin convolution is

but now if \(x {\gt} 2^\epsilon \), then the support of \(\nu _\epsilon \) is disjoint from the region of integration, and hence the integral is zero. We choose

By Lemma ??,

so

By Definitions 8, 6 and 7

and all the factors in the integrand are nonnegative.

By Definitions 8, 6 and 7

and since \(1_{(0,1]}(y)\le 1\), and all the factors in the integrand are nonnegative,

(because in mathlib the integral of a non-integrable function is \(0\), for the inequality above to be true, we must prove that \(\nu ((x/y)^{\frac1\epsilon })/y\) is integrable; this follows from the computation below). We then change variables to \(z=(x/y)^{\frac1\epsilon }\):

which by Theorem 7 is 1.

By Definition 8,

We wish to apply Theorem 6. To do so, we must prove that

is integrable on \([0,\infty )^2\). It is actually easier to do this for the convolution: \(\nu _\epsilon \ast 1_{(0,1]}\), so we use Lemma 45: for \(x\neq 0\),

Now, for \(x=0\), both sides of the equation are 0, so the equation also holds for \(x=0\). Therefore,

Now,

has compact support that is bounded away from \(y=0\) (specifically \(y\in [2^{-\epsilon },2^\epsilon ]\) and \(x\in (0,y]\)), so it is integrable. We can thus apply Theorem 6 and find

By Lemmas 10 and 9,

Use Lemma 52 and the bound in Lemma 8.

Follows from Lemmas 52, 7 and 47.

Use Lemma ?? to write \(\widetilde{1_{\epsilon }}(x)\) as an integral over an integral near \(1\), in particular avoiding the singularity at \(0\). The integrand may be bounded by \(2^{\epsilon }\nu _\epsilon (t)\) which is independent of \(x\) and we can use dominated convergence to prove continuity.

The function \((s - p)\cdot f(s)\) bounded, so by Theorem 3, there is a holomorphic function, \(g\), say, so that \((s-p)f(s) = g(s)\) in a neighborhood of \(s=p\), and \(g(p)=A\). Now because \(g\) is holomorphic, near \(s=p\), we have \(g(s)=A+O(s-p)\). Then when you divide by \((s-p)\), you get \(f(s) = A/(s-p) + O(1)\).

From ‘riemannZeta_residue_one‘ (in Mathlib), we know that \((s-1)\zeta (s)\) goes to \(1\) as \(s\to 1\). Now apply Theorem 11. (This can also be done using \(\zeta _0\) below, which is expressed as \(1/(s-1)\) plus things that are holomorphic for \(\Re (s){\gt}0\)...)

We know that \(f(s) = \frac{A}{s-p} + O(1)\) near \(p\), so we can write

The first term is bounded, say by \(M\), and the second term goes to \(\infty \) as \(s \to p\). Therefore, there exists a neighborhood \(V\) of \(p\) such that for all \(s \in V \setminus \{ p\} \), we have \(f(s) \neq 0\).

Using Theorem 3, there is a function \(g\) holomorphic near \(p\), for which \(f(s) = A/(s-p) + g(s) = h(s)/ (s-p)\). Here \(h(s):= A + g(s)(s-p)\) which is nonzero in a neighborhood of \(p\) (since \(h\) goes to \(A\) which is nonzero). Then \(f'(s) = (h'(s)(s-p) - h(s))/(s-p)^2\), and we can compute the quotient:

Since \(h\) is nonvanishing near \(p\), this remains bounded in a neighborhood of \(p\).

Elementary...

Elementary calculation.

The first term is \(g(s)(f(s) - \frac{A}{s - p})\), which is bounded near \(p\) by the assumption on \(f\) and the fact that \(g\) is holomorphic near \(p\). The second term is \(A\) times the log derivative of \(g\) at \(p\), which is bounded by the assumption that \(g\) is holomorphic.

This follows from Theorem 14 and Theorem 12.

Partial integration.

Apply Lemma 56 in blocks of length \(\le 1\).

Apply Lemma 57 to the function \(x \mapsto x^{-s}\).

Apply the triangle inequality

and evaluate the integral.

Apply Lemma 58 with \(a=N\) and \(b\to \infty \).

Apply Lemma 59 with \(a=N\) and \(b\to \infty \).

Apply Lemma 61 and estimate \(|s|\ll |t|\).

Apply Lemma 61 and estimate \(|s|\ll |t|\).

The function \(\zeta _0(N,s)\) is a finite sum of entire functions, plus an integral that’s absolutely convergent on \(\{ s\in \mathbb {C}\mid \Re (s){\gt}0 ∧ s \ne 1\} \) by Lemma 61.

Construct explicit paths from \(2\) to any point, either a line segment or two joined ones.

Use Lemma 60 and the Definition 9.

Use \(|n^{-s}| = n^{-\sigma } = e^{-\sigma \log n} \le \exp (-\left(1-\frac{A}{\log t}\right)\log n) \le n^{-1} e^A\), since \(n\le t\).

First replace \(\zeta (s)\) by \(\zeta _0(N,s)\) for \(N = \lfloor |t| \rfloor \). We estimate:

, where we used Lemma 67 and Lemma 62. The first term is \(\ll \log |t|\). For the second term, estimate

Estimate \(|s|= |\sigma + tI|\) by \(|s|\le 2 +|t| \le 2|t|\) (since \(|t|{\gt}3\)). Estimating \(|\left\lfloor x \right\rfloor +1/2-x|\) by \(1\), and using \(|x^{-s-1}| = x^{-\sigma -1}\), we have

For the last integral, integrate by parts, getting:

Now use \(\log N \le \log |t|\) to get the result.

First replace \(\zeta (s)\) by \(\zeta _0(N,s)\) for \(N = \lfloor |t| \rfloor \). Differentiating term by term, we get:

Estimate as before, with an extra factor of \(\log |t|\).

Zeta has a simple pole at \(s=1\). Equivalently, \(\zeta (s)(s-1)\) remains bounded near \(1\). Lots of ways to prove this. Probably the easiest one: use the expression for \(\zeta _0 (N,s)\) with \(N=1\) (the term \(N^{1-s}/(1-s)\) being the only unbounded one).

Split into two cases, use Lemma 71 for \(\sigma \) sufficiently small and continuity on a compact interval otherwise.

The identity

for \(\sigma {\gt}1\) is already proved by Michael Stoll in the EulerProducts PNT file.

Combine Lemma 73 with the bounds in Lemmata 72 and 68.

This is the fundamental theorem of calculus.

Use Lemma 75 and estimate trivially using Lemma 70.

Let \(\sigma \) be given in the prescribed range, and set \(\sigma ' := 1+ A / \log ^9 |t|\). Then

where we used Lemma 74 and Lemma 76. Now by making \(A\) sufficiently small (in particular, something like \(A = 1/16\) should work), we can guarantee that

as desired.

Follow same argument.

Apply Lemma 78.

Combine the bound on \(|\zeta '|\) from Lemma 70 with the bound on \(1/|\zeta |\) from Lemma 77.

This Lemma 80, but uniform in \(t\). The point is that the upper bound on \(\zeta ' / \zeta \) and the lower bound on \(\sigma \) only improve as \(|t|\) increases.

This fact is already proved in Stoll’s work.

Assume not. Then there is a sequence \(|t_n| \le T\) and \(\sigma _n \to 1\) so that \(\zeta (\sigma _n + it_n) = 0\). By compactness, there is a subsequence \(t_{n_k} \to t_0\) along which \(\zeta (\sigma _{n_k} + it_{n_k}) = 0\). If \(t_0\ne 0\), use the continuity of \(\zeta \) to get that \(\zeta (1 + it_0) = 0\); this is a contradiction. If \(t_0=0\), \(\zeta \) blows up near \(1\), so can’t be zero nearby.

The derivative of \(\zeta \) is holomorphic away from \(s=1\); the denominator \(\zeta (s)\) is nonzero in this range by Lemma 82.

The derivative of \(\zeta \) is holomorphic away from \(s=1\); the denominator \(\zeta (s)\) is nonzero in this range by Lemma 79.

Same as above.

Already in Mathlib.

By Lemma 53 the integrand is \(O(1/t^2)\) as \(t\rightarrow \infty \) and hence the function is integrable.

Interchange of summation and integration.

We have that

We have enough decay (thanks to quadratic decay of \(\mathcal{M}(\widetilde{1_{\epsilon }})\)) to justify the interchange of summation and integration. We then get

and apply the Mellin inversion formula (Theorem 5).

Take the difference. By Lemma 49 and 48, the sums agree except when \(1-c \epsilon \leq n/X \leq 1+c \epsilon \). This is an interval of length \(\ll \epsilon X\), and the summands are bounded by \(\Lambda (n) \ll \log X\).

Write as Dirichlet series and estimate trivially using Theorem 19.

The \(\zeta '(s)/\zeta (s)\) term is bounded, as is \(X^s\), and the smoothing function \(\mathcal{M}(\widetilde{1_{\epsilon }})(s)\) decays like \(1/|s|^2\) by Theorem 53. Actually, we already know that \(\mathcal{M}(\widetilde{1_{\epsilon }})(s)\) is integrable from Theorem 86, so we should just need to bound the rest.

Use the compactness of the rectangle and the fact that holomorphic functions are continuous.

Pull rectangle contours and evaluate the pole at \(s=1\).

Mimic the proof of Lemma 22.

Unfold the definitions and apply Lemma 54.

Elementary. Use ‘isLittleO_log_rpow_rpow_atTop‘ in Mathlib.

Unfold the definitions and apply the triangle inequality.

By Theorem 88 (once fixed!!), \(\zeta '/\zeta (\sigma _0 + t i)\) is bounded by \(\zeta '/\zeta (\sigma _0)\), and Theorem 17 gives \(\ll 1/(\sigma _0-1)\) for the latter. This gives:

where we used Theorem 53. Continuing the calculation, we have

where we used that \(\sigma _0=1+1/\log X\), and \(X^{\sigma _0} = X\cdot X^{1/\log X}=e \cdot X\).

Unfold the definitions and apply the triangle inequality.

where we used Theorems 53 and 81, and the fact that \(X^\sigma \le X^{\sigma _0} = X\cdot X^{1/\log X}=e \cdot X\). Since \(T{\gt}3\), we have \(\log T^9 \leq C''' T\).

Unfold the definitions and apply the triangle inequality.

where we used Theorems 53 and 80. Now we estimate \(X^{\sigma _1} = X \cdot X^{-A/ \log T^9}\), and the integral is absolutely bounded.

The analysis of \(I_4\) is similar to that of \(I_2\), (in Lemma 94) but even easier. Let \(C\) be the sup of \(-\zeta '/\zeta \) on the curve \(\sigma _2 + 3 i\) to \(1+ 3i\) (this curve is compact, and away from the pole at \(s=1\)). Apply Theorem 53 to get the bound \(1/(\epsilon |s|^2)\), which is bounded by \(C'/\epsilon \). And \(X^s\) is bounded by \(X^{\sigma _1} = X \cdot X^{-A/ \log T^9}\). Putting these together gives the result.

Here \(\zeta '/\zeta \) is absolutely bounded on the compact interval \(\sigma _2 + i [-3,3]\), and \(X^s\) is bounded by \(X^{\sigma _2}\). Using Theorem 53 gives the bound \(1/(\epsilon |s|^2)\), which is bounded by \(C'/\epsilon \). Putting these together gives the result.

Evaluate the integrals.