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

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 16, \(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 24, 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 24, 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 25).

Now apply Lemma 11.

We pull to a square with corners at \(-c-i*c\) and \(c+i*c\) for \(c{\gt}0\) sufficiently small. By Lemma 27, 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 7,

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

By Definitions 5 and 7

By (??) and Fubini’s theorem,

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

which, by Definition 5, 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 \(\psi \) 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 5 is

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

By Taylor’s theorem,

so, since \(\psi \) 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 \(\psi _\epsilon \) is

The support of \(\psi _\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 36. We then choose

which satisfies

by Lemma 38, so

Again the Mellin convolution is

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

By Lemma 38,

so

By Definitions 9, 7 and 8

and all the factors in the integrand are nonnegative.

By Definitions 9, 7 and 8

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 \(\psi ((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 9,

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: \(\psi _\epsilon \ast 1_{(0,1]}\), so we use Lemma 35: 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 43 and the bound in Lemma 8.

Follows from Lemmas 43, 7 and 37.

Partial integration.

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

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

Apply the triangle inequality

and evaluate the integral.

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

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

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

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

Use Lemma 50 and the Definition 10.

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 56 and Lemma 52. The first term is \(\ll \log |t|\). For the second term, estimate

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 59 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 61 with the bounds in Lemmata 60 and 57.

This is the fundamental theorem of calculus.

Use Lemma 63 and estimate trivially using Lemma 58.

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

where we used Lemma 62 and Lemma 64. 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 58 with the bound on \(1/|\zeta |\) from Lemma 65.

Already in Mathlib.

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 40 and 39, 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\).

[No longer relevant, as we will do better than any power of log savings...: This is not enough, as it loses a log! (Which is fine if our target is the strong PNT, with exp-root-log savings, but not here with the “softer” approach.) So we will need something like the Selberg sieve (already in Mathlib? Or close?) to conclude that the number of primes in this interval is \(\ll \epsilon X / \log X + 1\). (The number of prime powers is \(\ll X^{1/2}\).) And multiplying that by \(\Lambda (n) \ll \log X\) gives the desired bound.]

Pull rectangle contours.

Residue calculus / the argument principle.

Evaluate the integrals.