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 13, and rescale by \(c\); what remains is handled by Lemma 14.

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 20, \(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 28, 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 28, 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 29).

Now apply Lemma 15.

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 31, 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 41. 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 40: 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 47 and the bound in Lemma 8.

Follows from Lemmas 47, 7 and 42.

Partial integration.

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

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

Apply the triangle inequality

and evaluate the integral.

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

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

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

Apply Lemma 55 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 55.

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

Use Lemma 54 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 61 and Lemma 56. 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 65 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 67 with the bounds in Lemmata 66 and 62.

This is the fundamental theorem of calculus.

Use Lemma 69 and estimate trivially using Lemma 64.

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

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

as desired.

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

Same as above.

Already in Mathlib.

We have from Lemma 44 that \(\widetilde{1_{\epsilon }}(x) = 0\) for all \(x \leq 1+c\epsilon \). So the claimed function is integrable on \((0,\infty )\).

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

The function is a sum of continuous functions, and hence continuous.

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 44 and 43, 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\).

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

Residue calculus / the argument principle.

Evaluate the integrals.