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.

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.

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

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

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

Residue calculus / the argument principle.

Evaluate the integrals.