Let \(\sigma = \Re (s)\). By hypothesis, \(\sigma {\gt} 1\). By Lemma 404, we have \(|p^{-s}| = p^{-\sigma }\). Since \(p\in \mathcal{P}\), we have \(p\ge 2\). As \(\sigma {\gt}1\), it follows that \(p^\sigma {\gt} p^1 \ge 2\). Therefore, \(p^{-\sigma } = 1/p^\sigma {\lt} 1\).

Mathlib: riemannZeta_eulerProduct_hasProd, riemannZeta_eulerProduct_tprod,

Mathlib: abs_tprod

By ?? with \(P=\mathcal{P}\) and \(w(p) = (1-p^{-s})^{-1}\), which is multipiable.

By ??.

Mathlib: abs_inv

By lemma 385.

Apply lemma 389 and lemma 390 with \(z=1-p^{-s}\). Note \(z\neq 0\) by lemma 391.

By lemma 393 and assumption \(\Re (s){\gt}1\).

Apply Lemma 386 twice, to both \(\zeta (2s)\) and \(\zeta (s)\). Use condition lemma 394.

We proceed by cases on whether \(a\) ever takes the value zero.

Case 1: There exists \(p_0 \in P\) such that \(a(p_0) = 0\).

In this case, the infinite product \(\prod _{p \in P}' a(p)\) contains the factor \(a(p_0) = 0\), and therefore:

Similarly, the quotient function \(p \mapsto a(p)/b(p)\) satisfies \((a/b)(p_0) = a(p_0)/b(p_0) = 0/b(p_0) = 0\), so:

Therefore, both sides of the desired equality equal zero:

Case 2: For all \(p \in P\), \(a(p) \neq 0\).

In this case, our hypotheses are that both \(a\) and \(b\) are multipliable and map to non-zero values everywhere. Our strategy is to apply Assumption tprod_div, but doing so requires careful reasoning about the algebraic structures involved.

The Obstacle Assumption tprod_div requires the functions to map into a Commutative Group. The field of complex numbers, \({\mathbb C}\), is not a commutative group under multiplication because the element \(0\) lacks a multiplicative inverse. Therefore, we cannot directly apply the theorem to our functions \(a\) and \(b\).

The Strategy: Lifting to the Group of Units The solution is to work within the group of units of \({\mathbb C}\), denoted \({\mathbb C}^\times \), which is the set of non-zero complex numbers \({\mathbb C}\setminus \{ 0\} \). This set is a commutative group under multiplication. Since we are in the case where \(a(p)\) and \(b(p)\) are always non-zero, we can "lift" our functions to have \({\mathbb C}^\times \) as their codomain.

Defining the Lifted Functions We define two new unit-valued functions, \(u\) and \(v\):

These functions are well-defined because our case assumption (\(\forall p, a(p) \neq 0\)) and the given hypothesis (\(\forall p, b(p) \neq 0\)) guarantee their outputs are always in \({\mathbb C}^\times \).

Multipliability of the Lifted Functions The multipliability of \(u\) and \(v\) follows directly from that of \(a\) and \(b\). A function’s multipliability depends on the summability of \(|f(p) - 1|\) over its support. Since the values of \(u(p)\) and \(a(p)\) are identical (and likewise for \(v\) and \(b\)), their multipliability properties are preserved.

• \(\{ p : u(p) \neq 1\} = \{ p : a(p) \neq 1\} \) is countable (since \(a\) is multipliable).

• \(\sum _{p} |u(p) - 1| = \sum _{p} |a(p) - 1| {\lt} \infty \) (since \(a\) is multipliable).

• Similarly for \(v\) and \(b\).

Applying the Division Theorem With \(u\) and \(v\) established as multipliable functions into the commutative group \({\mathbb C}^\times \), we can now safely apply Assumption tprod_div. This gives us an equality that holds within \({\mathbb C}^\times \):

Returning to \({\mathbb C}\) Our final step is to show that this equality in \({\mathbb C}^\times \) implies the desired equality in \({\mathbb C}\). This is true because the natural inclusion (coercion) from \({\mathbb C}^\times \) to \({\mathbb C}\) preserves the algebraic operations of division and infinite products. Since \(\text{coe}(u(p)) = a(p)\) and \(\text{coe}(v(p)) = b(p)\), applying this coercion to both sides of Equation (??) directly yields our goal:

In both cases, the desired equality holds.

By lemma 396 with \(a(p)=(1-p^{-2s})^{-1}\) and \(b(p)=(1-p^{-s})^{-1}\). Multipliability holds by lemma 386, and use condition lemma 394.

By ??.

Basic algebra

By lemma 399, then invert terms and simplify. Note \(|z|{\lt}1\) implies \(z\neq \pm 1\) so we may invert \(1-z\) and \(1+z\) and \(1-z^2\).

Apply Lemma 398 and Lemma 400 with \(z=p^{-s}\). We verify condition using lemma 385.

Apply Theorem 401 with \(s=3/2\). Note \(\Re (3/2)=3/2{\gt}1\).

By the triangle inequality, \(|a+b| \le |a|+|b|\). Let \(a=1\) and \(b=-z\). Then \(|1-z| \le |1|+|-z| = 1+|z|\).

\(|p^{-s}| = |p^{-\sigma -it}| = |p^{-\sigma }p^{-it}| = |p^{-\sigma }||e^{-it\log p}| = p^{-\sigma } \cdot 1 = p^{-\sigma }\).

Apply Lemma 403 with \(z=p^{-(3/2+it)}\). This gives \(|1 - p^{-(3/2+it)}| \le 1 + |p^{-(3/2+it)}|\). Apply Lemma 404 with \(\sigma =3/2\) to get \(|p^{-(3/2+it)}| = p^{-3/2}\).

Basic property of inequalities

We have \(p^{-(3/2+it)}\neq 1\) by lemma 385 with \(s=3/2+it\).

Apply lemma 405, and then ?? with \(a = |1 - p^{-(3/2+it)}|\) and \(b=1 + p^{-3/2}\).

Mathlib: tprod_le_tprod

Apply ?? with \(P=\mathcal{P}\), \(a(p) = (1 + p^{-3/2})^{-1}\), \(b(p)=|1 - p^{-(3/2+it)}|^{-1}\). Multipliability holds by lemma 386

From Lemma 392 with \(s=3/2+it\), the left hand side is \(|\zeta (3/2+it)| = \prod '_{p\in \mathcal{P}}|1 - p^{-(3/2+it)}|^{-1}\). From Lemma 402, the right hand side is \(\frac{\zeta (3)}{\zeta (3/2)} = \prod '_{p\in \mathcal{P}}(1+p^{-3/2})^{-1}\). The theorem then follows directly from the inequality in Lemma 410.

By zeta_eq_tsum_one_div_nat_add_one_cpow, since \(x{\gt}1\) we have \(\zeta (x)=\sum _{n=1}^\infty n^{-x}\). Then note \(n^{-x}\) is positive real for all \(n\), so the sum is also positive real.

By lemma 412 applied twice, to both \(x=3\) and \(x=3/2\).

By theorem 411 with \(a=\frac{\zeta (3)}{\zeta (3/2)}\). Note \(a{\gt}0\) by lemma 413.

Mathlib: zeta_eq_tsum_one_div_nat_add_one_cpow

Mathlib: sum_mul_eq_sub_sub_integral_mul

Direct substution

By definition, \(\sum _{n=1}^{\lfloor u \rfloor } 1 = \lfloor u \rfloor \).

Apply the power rule for differentiation. See Mathlib/Analysis/Calculus.

Apply Lemma 417 with \(f(u)=u^{-s}\) and \(a_n=1\). Use lemma 418, and \(A(u)\) from Lemma 419, and \(f'(u)\) from Lemma 420.

By definition of the floor function.

Apply Lemma 421 and Lemma 422.

By definition of the fractional part function.

Apply Lemma 424 and linearity of the integral.

Apply Lemmas 423 and 425.

The antiderivative of \(u^{-s}\) is \(\frac{u^{1-s}}{1-s}\). Evaluate at \(u=N\) and \(u=1\).

Apply Lemmas 426 and 427 and combine terms: \(N^{1-s} + \frac{s}{1-s}N^{1-s} = N^{1-s}(1+\frac{s}{1-s}) = N^{1-s}(\frac{1-s+s}{1-s}) = \frac{N^{1-s}}{1-s}\). The term \(-\frac{s}{1-s}\) is \(\frac{s}{s-1}=1+\frac{1}{s-1}\).

\(|N^{1-s}| = N^{1-\Re (s)}\). Since \(1-\Re (s) {\lt} 0\), this limit tends to 0.

By definition of the fractional part.

Apply Lemma 430. We have \(|\{ u\} u^{-s-1}| = |\{ u\} | |u^{-s-1}| \le 1 \cdot u^{-\Re (s)-1}\).

Apply Lemma 431 and that \(x\mapsto u^{-1-x}\) is monotonic.

Standard results from complex analysis.

By Lemmas 433 and 432, we calculate

Thus the integral converges.

Take the limit \(N\to \infty \) in Lemma 428. Apply Lemmas 415, 429, and 434.

Apply lemma 464

\(S\) is the complement of the singleton \(\{ 1\} \), which is open.

\(T\) is the intersection of the open set \(S\) with the open half-plane \(\{ s : \Re (s) {\gt} 1/10\} \).

The set \(T\) can be shown to be path-connected, which implies preconnected.

Take \(s\in T\). The function \(\frac{z}{z-1}\) is analyticAt \(z=s\), since \(s\neq 1\). The integral converges uniformly by lemma 434, so \(F(z)\) is analyticAt \(z=s\).

Direct algebraic manipulation: \(\frac{z}{z-1} = \frac{(z-1)+1}{z-1} = \frac{z-1}{z-1} + \frac{1}{z-1} = 1 + \frac{1}{z-1}\).

By Lemma 435, the equality \(\zeta (s)=F(s)\) holds for \(\Re (s){\gt}1\). By Lemma 441, \(F(s)\) is analyticOnNhd \(T\). By Lemma 436 \(\zeta (s)\) is analyticOnNhd \(S\supset T\). Hence by the identity principle, (Mathlib try AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq) the equality \(\zeta (s)=F(s)\) holds in \(T\).

Apply Lemma 433 to the formula in Lemma 443.

The antiderivative is \(\frac{u^{-\Re (s)}}{-\Re (s)}\). Evaluating from \(1\) to \(\infty \) gives \(0 - \frac{1}{-\Re (s)} = \frac{1}{\Re (s)}\).

Apply Lemmas 444, 431, and 445.

Algebraic identity and Lemma 433.

Apply Lemmas 446 and 447.

\(|s|^2 = \sigma ^2+t^2 \le 3^2+t^2 = 9+|t|^2\). Since \(0 \le 6|t|\), we have \(9+|t|^2 \le 9+6|t|+|t|^2 = (3+|t|)^2\). Taking the square root gives \(|s| \le 3+|t|\).

From \(1/2 \le \Re (s)\), taking reciprocals reverses the inequality.

\(|s-1|^2 = (\sigma -1)^2 + t^2\). Since \(|t|\ge 1\), \(t^2\ge 1\). Since \((\sigma -1)^2 \ge 0\), we have \(|s-1|^2 \ge 1\).

In Lemma 448, apply Lemma 451 to bound \(\frac{1}{|s-1|} \le 1\). Apply Lemma 449 to bound \(|s|\) and Lemma 450 to bound \(\frac{1}{\Re (s)}\).

By arithmetic. \(2 + 6 + 2|t| = 8+2|t|\).

Apply Lemmas 452 and 453.

Direct calculation

Apply lemma 455, and use arithmetic. Here \(\Im (s)^2 + \Re (s)^2 = |s|^2 \in [0,1]\) by assumption.

Apply ??.

Mathlib: DifferentiableAt.differentiableWithinAt

Unfold definition of DifferentiableOn \(T\) in terms of differentiableWithinAt \(s\) for all \(s\in T\).

By ??

Mathlib: Complex.analyticOnNhd_iff_differentiableOn

By ??

Apply ?? with \(T=S\) and \(g(s)=\zeta (s)\).

For sake of contradiction, suppose \(s=1\). Then we calculate

Thus \(|s-c| \ge |t|{\gt}1\), but this contradicts \(|s-c|\le 1\). Hence the proof is complete.

By lemma 465, and unfolding the definitions of \(c\), \(\overline{{\mathbb D}}_1(c)\), and \(S\).

Apply ??, and then Mathlib: AnalyticOnNhd.mono

By lemma 468

Since \(f\) is AnalyticOnNhd \(\overline{{\mathbb D}}_1(c)\), and \(\overline{{\mathbb D}}_1(c)=\{ z+c:z\in \overline{{\mathbb D}}_1\} \), then \(f_c\) is AnalyticOnNhd \(\overline{{\mathbb D}}_1\).

Next we calculate \(f_c(0) = \frac{f(0+c)}{f(c)} = \frac{f(c)}{f(c)} = 1.\)

By the chain rule, we calculate \(f_c'(z) = f'(z+c)\). Thus since \(f(c),f(z+c) \neq 0\), we calculate

If \(z\overline{{\mathbb D}}_R\) then \(z+c\in \overline{{\mathbb D}}_R\), so \(|f(z+c)|\le B\) by assumption. Thus we calculate \(|f_c(z)| = |f(z+c)|/f(c) \le B/|f(c)|\).

By definition, \(\rho ' \in \mathcal{K}_{f_c}(r)\) means \(f_c(\rho ')=0\) and \(|\rho '|\le r\). By definition of \(f_c\) we have \(f_c(\rho ')=f(\rho '+c)/f(c)\). Since \(f(c)\neq 0\) we conclude \(f(\rho '+c)=0\). Also \(|(\rho '+c)-c|=|\rho '|\le r\), and hence \(\rho '+c \in \mathcal{K}_{f}(r;c)\). Therefore \(\rho ' \in \mathcal{K}_{f_c}(r)\) implies \(\rho '+c \in \mathcal{K}_{f}(r;c)\)

The proof that \(\rho \in \mathcal{K}_{f}(r;c)\) implies \(\rho -c \in \mathcal{K}_{f_c}(r)\) is similar.

By definition of analyticOrderAt, we have \(f_c(z) = (z-\rho )^{m_{\rho ,f_c}} h(z)\) for some \(h\) AnalyticAt \(\rho \) with \(h(\rho )\neq 0\). As \(f_c(z) = f(z+c)/f(c)\) and \(f(c)\neq 0\), this implies \(f(z+c) = (z-\rho ')^{m_{\rho ',f_c}} h(z)f(c)\). Thus letting \(w=z+c\) and \(g(w) = h(w-c)f(c)\), we have \(f(w) = (w-c-\rho )^{m_{\rho ,f_c}} g(w)\). Observe \(h\) AnalyticAt \(\rho '\) implies that \(g\) is AnalyticAt \(\rho '+c\). And \(h(\rho '),f(c)\neq 0\) imply \(g(\rho +c)\neq 0\). Hence by definition we conclude AnalyticAt of \(f\) at \(\rho +c\) equals \(m_{\rho ',f_c}\).

First \(z\in \overline{{\mathbb D}}_{r_1}\) if and only if \(|z| \le r_1\) if and only if \(|(z+c)-c|\le r_1\) iff \(z+c\in \overline{{\mathbb D}}_{r_1}(c)\). Second, since \(f(c)\neq 0\) we have \(z\in \mathcal K_{f_c}(R_1)\) if and only if \(f_c(z)=0\) if and only if \(f(z+c)=0\) if and only if \(z+c\in \mathcal K_{f}(R_1;c)\). Combining these two equivalences, \(z\in \overline{{\mathbb D}}_{r_1} \setminus \mathcal K_{f_c}(R_1)\) if and only if \(z+c\in \overline{{\mathbb D}}_{r_1}(c) \setminus \mathcal K_{f}(R_1;c)\).

Apply lemma 383 with the function \(f_c\), using the conditions ??.

We apply lemma 476 using \(f(z) = \zeta (z)\). The conditions \(\zeta \) AnalyticOnNhd \(\overline{{\mathbb D}}_1(c)\) with \(\zeta (c)\neq 0\) hold by ??.

Euler product for zeta, triangle inequality, properties of \(\zeta (\sigma )\) for \(\sigma {\gt}1\) Let \(s = \sigma + it\). We are interested in the case where \(\sigma = 3/2\).

Step 1: Use the Euler Product Formula

For any complex number \(s\) with \(\Re (s) = \sigma {\gt} 1\), the Riemann zeta function can be represented by the absolutely convergent Euler product over all prime numbers \(p\):

This implies that its reciprocal is

We take the modulus of both sides:

Step 2: Bound the term \(|1-p^{-s}|\)

Using the triangle inequality (\(|z_1+z_2| \le |z_1|+|z_2|\)), we can bound each term in the product:

The modulus of \(p^{-s}\) is:

So, we have \(|1-p^{-s}| \le 1+p^{-\sigma }\).

Step 3: Bound the entire product

Substituting this back into the product for the reciprocal’s modulus:

The product \(\prod _{p} (1+p^{-\sigma })\) can be expanded:

This expanded sum contains terms \(n^{-\sigma }\) for all square-free integers \(n\). This sum is strictly less than the sum over all integers \(n \ge 1\):

The sum on the right is, by definition, the Riemann zeta function evaluated at the real number \(\sigma \), i.e., \(\zeta (\sigma )\). Thus, we have established that for \(\sigma {\gt} 1\):

Step 4: Conclude the proof

Taking the reciprocal of the inequality (and flipping the inequality sign) gives:

We are interested in the specific case \(\sigma = 3/2\). For this value, we have:

The value \(\zeta (3/2) = \sum _{n=1}^\infty n^{-3/2}\) is a convergent sum of positive terms, so it is a finite positive constant (approximately 2.612). We can therefore define our constant \(a\) to be \(a = 1/\zeta (3/2)\). Since \(\zeta (3/2){\gt}0\), we have \(a{\gt}0\). The inequality \(|\zeta (3/2+it)| \ge a\) holds for all \(t \in {\mathbb R}\).

Let \(a{\gt}0\) be as in lemma 478, so \(|\zeta (3/2+it)| \ge a\) for all \(t\in {\mathbb R}\). Set \(A = \max \{ 2, \log (1/a)\} \). Clearly \(A {\gt} 1\) since \(a {\gt} 0\) and \(\log (1/a) {\gt} 0\). For any \(t\in {\mathbb R}\), set \(x = |\zeta (3/2+it)|\). Then \(a \leq x\), so \(1/x \leq 1/a\) and \(\log (1/x) \leq \log (1/a) \leq A\). Also, \(\log (1/x) {\lt} 2 \leq A\) for \(x {\gt} 1/2\). Thus \(\log (1/x) \leq A\) for all \(t\).

Apply lemma 457

The proof of this lemma is a direct application of lemma 480 by a change of variables.

Step 1: Recall the prerequisite lemma

Lemma 480 states that there exists a constant \(b{\gt}1\) such that for all \(t\in {\mathbb R}\) with \(|t|\ge 3\) and for all complex numbers \(s_{pre}\in {\mathbb C}\) with \(|s_{pre}|\le 1\), the following inequality holds:

We will show that the conditions and conclusion of the current lemma perfectly align with this statement.

Step 2: Unpack the conditions of the current lemma

We are given the following conditions:

1. A real number \(t\) with \(|t| {\gt} 3\).

2. A complex number \(c = 3/2 + it\).

3. A complex number \(s\) which belongs to the closed disk of radius 1 centered at \(c\), denoted \(\overline{{\mathbb D}}_1(c)\).

The condition \(s \in \overline{{\mathbb D}}_1(c)\) means, by definition, that the distance between \(s\) and \(c\) is at most 1:

Step 3: Define a new variable to match the prerequisite

Our goal is to bound \(|\zeta (s)|\). Let’s define a new variable, which we will call \(s_{pre}\), in a way that relates our \(s\) to the argument of the zeta function in lemma 480. Let’s set the argument of \(\zeta \) in our lemma, which is \(s\), equal to the argument of \(\zeta \) in the prerequisite lemma, which is \(s_{pre}+3/2+it\):

Now, let’s solve for \(s_{pre}\):

Recognizing the definition \(c=3/2+it\), this simplifies to:

Step 4: Verify the conditions on the new variable

Lemma 480 requires that the variable \(s_{pre}\) satisfies \(|s_{pre}| \le 1\). Let’s check if our definition of \(s_{pre}\) meets this condition. From Step 2, we know that for any \(s \in \overline{{\mathbb D}}_1(c)\), we have \(|s - c| \le 1\). Substituting our definition from Step 3, this is exactly the condition:

Therefore, for any \(s\) that satisfies the conditions of our lemma, we can define \(s_{pre} = s-c\), and this \(s_{pre}\) will satisfy the conditions of lemma 480.

Step 5: Apply the prerequisite lemma and conclude

We have established the following:

• We are given \(t\) with \(|t|{\gt}3\). This matches the condition on \(t\) in lemma 480.

• For any \(s \in \overline{{\mathbb D}}_1(c)\), we can write \(s = s_{pre} + c = s_{pre} + 3/2 + it\), where \(s_{pre} = s-c\) satisfies \(|s_{pre}| \le 1\).

We can now apply the inequality from lemma 480 to the number \(\zeta (s_{pre} + 3/2 + it)\). The lemma guarantees the existence of a constant \(b{\gt}1\) such that:

Since \(s = s_{pre} + 3/2 + it\), this inequality is identical to:

This holds for any \(s \in \overline{{\mathbb D}}_1(c)\) and any \(t \in {\mathbb R}\) with \(|t|{\gt}3\). This is precisely the statement we needed to prove.

We apply ?? with \(B=bt\), and \(C_1=C/R\).

We apply lemma 482 and choose \(R_1 = 5/6\), \(R=8/9\). Set \(C=\left(16 + \frac{1}{(R^2/R_1 - R_1)\log (R/R_1)}\right)(1 + \log (b) + A)\).