Follows directly from the definitions.

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.1.2. To evaluate the integral of \(1/(s-p)\), pull everything to a square about the origin using Lemma 4.1.2, and rescale by \(c\); what remains is handled by Lemma 4.1.3.

Obvious.

Almost by definition.

Almost by definition.

Almost by definition.

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

So pulling contours gives \(\int _{(\sigma )}=0\).

By ring.

Applying Lemma 4.2.17, 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 4.2.17, 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 4.2.18).

Now apply Lemma 4.1.4.

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

So pulling contours gives \(\int _{(-3/2)}=0\).

Partial integration.

By Definition 4.3.1,

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

By Definitions ?? and 4.3.1

By (??) and Fubini’s theorem,

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

which, by Definition ??, is

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 4.3.1,

which by Definition ?? 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 4.3.5.

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 4.3.3. 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 4.3.3, 4.3.1 and 4.3.2

and all the factors in the integrand are nonnegative.

By Definitions 4.3.3, 4.3.1 and 4.3.2

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 4.3.5 is 1.

By Definition 4.3.3,

We wish to apply Theorem 4.3.1. 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 4.3.2: 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 4.3.1 and find

By Lemmas 4.3.4 and 4.3.3,

Use Lemma 4.3.9 and the bound in Lemma 4.3.2.

Follows from Lemmas 4.3.9, 4.3.1 and 4.3.4.

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.

Same idea as Urysohn-type argument.

We proceed by case analysis on whether \(f\) is differentiable at \(p\). If \(f\) is differentiable at \(p\), then we can apply the previous theorem. If \(f\) is not differentiable at \(p\), then neither is \(g\), and both derivatives have the default value of zero.

We apply the derivative conjugation symmetry to the Riemann zeta function and use the conjugation symmetry of the Riemann zeta function itself.

We unfold the interval integral into an integral over a uIoc and use the conjugation property of integrals.

The function \((s - p)\cdot f(s)\) bounded, so by Theorem 4.1.1, 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 4.4.4. (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 4.1.1, 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 4.4.7 and Theorem 4.4.5.

This is first order Euler-Maclaurin.

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

Apply the triangle inequality

and evaluate the integral.

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

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

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

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

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

Use Lemma 4.4.4 and the Definition 4.4.1.

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 4.4.10 and Lemma 4.4.6. 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 4.4.14 for \(\sigma \) sufficiently small and continuity on a compact interval otherwise.

Combine Lemma ?? with upper bounds for \(|\zeta (\sigma )|\) (from Lemma 4.4.15) and \(|\zeta (\sigma +2it)|\) (from Lemma 4.4.11).

The identity

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

Combine Lemma 4.4.17 with the bounds in Lemmata 4.4.15 and 4.4.11.

This is the fundamental theorem of calculus.

Use Lemma 4.4.19 and estimate trivially using Lemma 4.4.13.

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

where we used Lemma 4.4.18 and Lemma 4.4.20. 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 4.4.22.

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

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 4.4.25.

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

For \(\sigma \) close to \(1\) use Lemma 4.4.24, otherwise estimate trivially.

Already in Mathlib.

By Lemma 4.3.10 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.

Take the difference. By Lemma 4.3.6 and 4.3.5, 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 4.5.1.

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 4.3.10. Actually, we already know that \(\mathcal{M}(\widetilde{1_{\epsilon }})(s)\) is integrable from Theorem 4.5.1, 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 4.5.4.

Unfold the definitions and apply Lemma 4.3.11.

We use the fact that \(\log ^k X / X\) goes to \(0\) as \(X \to \infty \). Then we use the extreme value theorem to find a constant \(C\) that works for all \(X \geq X_0\).

Unfold the definitions and apply the triangle inequality.

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

where we used Theorem 4.3.10. 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\).

We deduce this from the corresponding bound for \(I_1\), using the symmetry between \(I_1\) and \(I_9\).

Unfold the definitions and apply the triangle inequality.

where we used Theorems 4.3.10, the hypothesised bound on zeta 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^{n_2} \leq C''' T\).

This is a direct consequence of the definitions of \(I_2\) and \(I_8\).

We deduce this from the corresponding bound for \(I_2\), using the symmetry between \(I_2\) and \(I_8\).

By Real.log_le_sub_one_of_pos we know that \(\log y\leq y-1\). If we set \(y=x^{1/c}\) this becomes

Multiplying through by \(c\) we have

as desired.

Using the previous lemma, we know for all \(0{\lt}c\) and \(0{\lt}x\) that

Now if we choose \(c=2n\) then

This function is dominates the integrand and is integrable in \(x\) by the \(p\)-test.

Unfold the definitions and apply the triangle inequality.

where we used Theorems 4.3.10 and the hypothesised bound on zeta. Now we estimate \(X^{\sigma _1} = X \cdot X^{-A/ \log T^{n_1}}\), and the integral is absolutely bounded.

We deduce this from the corresponding bound for \(I_3\), using the symmetry between \(I_3\) and \(I_7\).

The analysis of \(I_4\) is similar to that of \(I_2\), (in Lemma ??) 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 4.3.10 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^{n_1}}\). Putting these together gives the result.

We deduce this from the corresponding bound for \(I_4\), using the symmetry between \(I_4\) and \(I_6\).

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 4.3.10 gives the bound \(1/(\epsilon |s|^2)\), which is bounded by \(C'/\epsilon \). Putting these together gives the result.

By Theorems 4.5.4, 4.5.6, and 4.5.3 we have that

Applying Theorems 4.5.8, 4.5.10, 4.5.15, 4.5.17, 4.5.19, 4.5.18, 4.5.16, 4.5.12, 4.5.9, and 4.3.11 we have

Balancing the error terms in \(\varepsilon \) and \(T\) completes the proof.

This follows as a corollary of Theorems 4.6.1 and 4.4.24.