2 Proof

Definition 2.1

✓

\[ P_n(x):=\frac{1}{n!}\frac{d^n}{dx^n}[x^n(1-x)^n] \]

Lemma 2.2

\[ P_n(x)=\sum \limits _{k=0}^{n}(-1)^k\binom {n}{k}\binom {n+k}{n}x^k \]

Hence \(P_n(x)\) is integer polynomial.

Proof ▶

\begin{align*} \frac{1}{n!}\frac{d^n}{dx^n}[x^n(1-x)^n] & = \frac{1}{n!}\frac{d^n}{dx^n}[(x-x^2)^n]\\ & = \frac{1}{n!}\frac{d^n}{dx^n}[\sum \limits _{k=0}^{n} \binom {n}{k}(-1)^k x^{n-k}x^{2k}]\\ & = \frac{1}{n!}\frac{d^n}{dx^n}[\sum \limits _{k=0}^{n} \binom {n}{k}(-1)^k x^{n+k}]\\ & = \frac{1}{n!}\sum \limits _{k=0}^{n} \binom {n}{k}(-1)^k \frac{d^n}{dx^n}[x^{n+k}]\\ & = \frac{1}{n!}\sum \limits _{k=0}^{n} \binom {n}{k}(-1)^k \frac{(n+k)!}{k!}x^{k}\\ & = \sum \limits _{k=0}^{n} \binom {n}{k}(-1)^k \frac{1}{n!}\frac{(n+k)!}{k!}x^{k}\\ & = \sum \limits _{k=0}^{n} (-1)^k \binom {n}{k}\binom {n+k}{n}x^{k} \end{align*}

Lemma 2.3

For \( 0 {\lt} x, z {\lt} 1\),,

\[ \frac{\partial ^n}{\partial y^n}(\frac{1}{1 - (1-xy)z}) = \frac{(-1)^nn!(xz)^n}{(1 - (1-xy)z)^{n+1}} \]

Proof ▶

By definition.

Lemma 2.4

For all \( 0 {\lt} x, z {\lt} 1\), one has

\[ \int _{0}^{1}\frac{P_n(y)}{1 - (1-xy)z} \, dx =(-1)^n \int _{0}^{1} \frac{(xyz)^n(1-y)^n}{(1 - (1-xy)z)^{n+1}} \, dx \]

Proof ▶

By induction and integration by parts.

Lemma 2.5

For all \(n \in \mathbb {R}, n {\gt} -1\),

\[ \int _{0}^{1} -{\rm ln}(x) x^n = \frac{1}{(n + 1)^2} \, dx \]

Proof ▶

\begin{align*} \int _{0}^{1} -{\rm ln}(x)\cdot x^n =& \frac{x^{n+1}}{(n+1)^2} - \frac{{\rm ln}(x) x^{n+1}}{n+1} |_0^1 \\ =& \frac{1}{(n+1)^2} \end{align*}

Lemma 2.6

For all \(k,s,r \in \mathbb {N}\),

\[ -\int _{0}^{1}\int _{0}^{1} {\rm ln}(xy)x^{k+r}y^{k+s}\, dx \, dy = \frac{1}{((k+r+1)^2(k+s+1))}+\frac{1}{((k+r+1)(k+s+1)^2)} \]

Proof ▶

\begin{align*} & -\int _{0}^{1}\int _{0}^{1} {\rm ln}(xy)x^{k+r}y^{k+s}\, dx \, dy \\ =& \int _{0}^{1}\int _{0}^{1} -{\rm ln}(x)x^{k+r}y^{k+s}\, dx \, dy + \int _{0}^{1}\int _{0}^{1} -{\rm ln}(y)x^{k+r}y^{k+s}\, dx \, dy \\ =& \int _{0}^{1} \frac{-{\rm ln}(x)x^{k+r}}{k+s+1} \, dx + \int _{0}^{1}\int _{0}^{1} \frac{x^{k+r}}{(k+s+1)^2}\, dx\\ =& \frac{1}{((k+r+1)^2(k+s+1))} + \frac{1}{((k+r+1)(k+s+1)^2)} \end{align*}

Lemma 2.7

For all \(r,s \in \mathbb {N}\),

\[ J_rs = \sum _{k \in \mathbb {N}} \frac{1}{((k+r+1)^2(k+s+1))}+\frac{1}{((k+r+1)(k+s+1)^2)} \]

Proof ▶

\begin{align*} J_rs =& -\int _{0}^{1}\int _{0}^{1} x^ry^s{\rm ln}(xy) \sum _{k=0}^{\infty } (xy)^k \, dx \, dy \\ =& \sum _{k=0}^{\infty } -\int _{0}^{1}\int _{0}^{1} x^ry^s{\rm ln}(xy)(xy)^k \, dx \, dy \\ =& \sum _{k=0}^{\infty } -\int _{0}^{1}\int _{0}^{1} {\rm ln}(xy)x^{k+r}y^{k+s} \, dx \, dy \\ =& \sum _{n \in \mathbb {N}} \frac{1}{((k+r+1)^2(k+s+1))}+\frac{1}{((k+r+1)(k+s+1)^2)} \end{align*}

Lemma 2.8

\[ J_{00} := -\int _{0}^{1}\int _{0}^{1} \frac{{\rm ln}(xy)}{1-xy} \, dx \, dy = 2\zeta (3) \]

Proof ▶

Obvious.

Lemma 2.9

for all integers \(r {\gt} 0\)

\[ J_{rr} := -\int _{0}^{1}\int _{0}^{1} x^ry^r\frac{{\rm ln}(xy)}{1-xy} \, dx \, dy = 2\zeta (3) - 2 \sum \limits _{m = 1}^{r}\frac{1}{m^3} \]

Proof ▶

By Simplification.

Lemma 2.10

Let \(r\) and \(s\) be non-negative integers, with \(r \neq s\), then

\[ J_{rs} := -\int _{0}^{1}\int _{0}^{1} x^ry^s\frac{{\rm ln}(xy)}{1-xy} \, dx \, dy = \frac{\sum \limits _{m = 1}^{r}\frac{1}{m^2} - \sum \limits _{m = 1}^{s}\frac{1}{m^2}}{r - s} \]

Proof ▶

By Simplification.

Lemma 2.11

For all \(r \in \mathbb {N}^*, d_n\) is lcm of \(\{ 1, 2, \ldots , n\} .\)

\[ d_{r^3} = (d_r)^3 \]

Proof ▶

By prime factor expand.

Lemma 2.12

For all \(r \in \mathbb {N}^*\),

\[ J_{rr} = 2 \zeta (3) - \frac{z_r}{(d_r)^3} \]

for some \(z_r \in \mathbb {Z}\).

Proof ▶

By computing.

Lemma 2.13

For all \(r \in \mathbb {N}^*, d_n\) is lcm of \(\{ 1, 2, \ldots , n\} .\)

\[ d_{r^2} = (d_r)^2 \]

Proof ▶

By prime factor expand.

Lemma 2.14

For all \(r \in \mathbb {N}, r \neq s\),

\[ J_{rs} = \frac{z_{rs}}{(d_r)^3} \]

for some \(z_{rs} \in \mathbb {Z}\).

Proof ▶

By computing.

Lemma 2.15

\[ \int _{0}^{1} \frac{1}{1 - (1 - x)z} \, dz= -\frac{{\rm ln}x}{1 - x} \]

Proof ▶

Substitute \(y = (1 - x)z\) in the integral, and we also have \(dy = (1-x)dz\). Then we deduce that

\begin{align*} \int _{0}^{1} \frac{1}{1 - (1 - x)z} \, dz =& \int _{0}^{1-x} \frac{1}{(1 - y)(1-x)} \, dy \\ =& \frac{1}{1-x}\int _{0}^{1-x} \frac{1}{1 - y} \, dy\\ =& \frac{1}{1-x}[-{\rm ln}(1-y)]_0^{1-x} \\ =& \frac{1}{1-x}[-{\rm ln}(x) + {\rm ln}(1)] \\ =& -\frac{{\rm ln}x}{1 - x} \end{align*}

Definition 2.16

✓

\[ JJ_n := - \int _{0}^{1}\int _{0}^{1} P_n(x)P_n(y)\frac{{\rm ln}(xy)}{1-xy} \, dx \, dy \]

Lemma 2.17

For some integers \(a_n\) and \(b_n\),

\[ JJ_n = \frac{a_n}{d_n^3} + b_n\zeta (3) \]

Proof ▶

Since \(P_n(x) \in \mathbb {Z}[x]\). Suppose \(P_n(x) = \sum \limits _{k=0}^{n}a_kx^k\), where \(a_k \in \mathbb {Z}\).
Then

\begin{align*} JJ_n & = -\int _{0}^{1}\int _{0}^{1} P_n(x)P_n(y)\frac{{\rm ln}(xy)}{1-xy} \, dx \, dy \\ & = -\int _{0}^{1}\int _{0}^{1} \sum \limits _{i=0}^{n}a_ix^i \sum \limits _{j=0}^{n}a_jy^j \frac{{\rm ln}(xy)}{1-xy} \, dx \, dy\\ & = \sum \limits _{i=0}^{n}\sum \limits _{j=0}^{n}a_i a_j -\int _{0}^{1}\int _{0}^{1} x^i y^j \frac{{\rm ln}(xy)}{1-xy} \, dx \, dy\\ & = \sum \limits _{i=0}^{n}\sum \limits _{j=0}^{n}a_i a_j J_{ij}\\ \end{align*}

We have \(J_{rr}\) and \(J_{rs} \in \mathbb {Z}\zeta (3) + \frac{\mathbb {Z}}{d_n^3}\).
So \(JJ_n \in \mathbb {Z}\zeta (3) + \frac{\mathbb {Z}}{d_n^3}\).

Definition 2.18

✓

\[ JJ'_n := - \int _{0}^{1}\int _{0}^{1}\int _{0}^{1} (\frac{x(1-x)y(1-y)z(1-z)}{1-(1-yz)x})^n \frac{1}{1-(1-yz)x} \, dx \, dy \, dz \]

Lemma 2.19

Let \(D = \{ (x,y,z)|x,y,z\in (0,1)\} \), then

\[ \frac{x(1-x)y(1-y)z(1-z)}{(1-(1-xy)z)} {\lt} \frac{1}{24} \]

Proof ▶

We have an inequality

\[ 1-(1-xy)z = 1-z + xyz \geqslant 2\sqrt{1-z}\sqrt{xyz} \]

Then we can deduce that for \((x,y,z) \in D\),

\begin{align*} \frac{x(1-x)y(1-y)z(1-z)}{(1-(1-xy)z)} \leqslant & \frac{x(1-x)y(1-y)z(1-z)}{2\sqrt{1-z}\sqrt{xyz}}\\ =& \frac{\sqrt{x}(1-x)\sqrt{y}(1-y)\sqrt{z}\sqrt{1-z}}{2} \end{align*}

For \(z\in (0,1)\), the max value of \(\sqrt{z}\sqrt{1-z} = \sqrt{z(1-z)}\) is got at \(z=\frac{1}{2}\). And for \(y \in (0,1)\), we have \(y(1-y)^2 - \frac{4}{27} = (y - \frac{4}{3})(y - \frac{1}{3})^2 \leqslant 0\). Then

\[ \sqrt{y}(1-y) = \sqrt{y(1-y)^2} \leqslant \sqrt{\frac{4}{27}} \leqslant \sqrt{\frac{4}{25}} = \frac{2}{5} \]

Then we have

\begin{align*} \frac{x(1-x)y(1-y)z(1-z)}{(1-(1-xy)z)} \leqslant & \frac{2}{5}\cdot \frac{2}{5}\cdot \frac{1}{2}\cdot \frac{1}{2} \\ =& \frac{1}{25} {\lt} \frac{1}{24} \end{align*}

Lemma 2.20

For \(0 {\lt} z {\lt} 1\),

\[ \int _{0}^{1}\int _{0}^{1} P_n(x)P_n(y) \frac{1}{1 - (1 - xy)z} \, dx \, dy = \int _{0}^{1}\int _{0}^{1} \frac{P_n(x)(xyz)^n(1-y)^n}{(1-(1-xy)z)^{n + 1}} \, dx \, dy \]

Proof ▶

Lemma 2.21

For \(0 {\lt} x, y {\lt} 1\),

\[ \int _{0}^{1} \frac{P_n(x)(xyz)^n(1-y)^n}{(1-(1-xy)z)^{n + 1}} \, dz = \int _{0}^{1} \frac{P_n(x)(1-z)^n(1-y)^n}{1-(1-xy)z} \, dz \]

Proof ▶

Lemma 2.22

For \(0 {\lt} z {\lt} 1\),

\[ \int _{0}^{1}\int _{0}^{1} \frac{P_n(x)(1-y)^n}{1-(1-xy)z} \, dx \, dy = \int _{0}^{1}\int _{0}^{1} \frac{(xyz(1-x)(1-y))^n}{(1-(1-xy)z)^{n+1}} \, dx \, dy \]

Proof ▶

Theorem 2.23

\[ JJ_n = JJ'_n \]

Proof ▶

\begin{align*} JJ_n & = \int _{0}^{1}\int _{0}^{1} P_n(x)P_n(y)(\int _{0}^{1} \frac{1}{1 - (1 - xy)z} \, dz) \, dx \, dy \\ & =\int _{0}^{1}\int _{0}^{1}\int _{0}^{1} P_n(x)P_n(y) \frac{1}{1 - (1 - xy)z} \, dx \, dy \, dz \\ & =\int _{0}^{1}\int _{0}^{1}\int _{0}^{1} \frac{P_n(x)(xyz)^n(1-y)^n}{(1-(1-xy)z)^{n + 1}} \, dx \, dy \, dz \\ & =\int _{0}^{1}\int _{0}^{1}\int _{0}^{1} \frac{P_n(x)(1-z)^n(1-y)^n}{1-(1-xy)z} \, dz \, dx \, dy \\ & =\int _{0}^{1} (1-z)^n (\int _{0}^{1}\int _{0}^{1} \frac{P_n(x)(1-y)^n}{1-(1-xy)z} \, dx \, dy) \, dz \\ & =\int _{0}^{1} (1-z)^n (\int _{0}^{1}\int _{0}^{1} \frac{(xyz(1-x)(1-y))^n}{(1-(1-xy)z)^{n+1}} \, dx \, dy) \, dz \\ & =\int _{0}^{1}\int _{0}^{1}\int _{0}^{1} \frac{(xyz(1-x)(1-y)(1-z))^n}{(1-(1-xy)z)^{n+1}} \, dz \, dx \, dy & =JJ’_n \end{align*}

Theorem 2.24

\[ 0 {\lt} JJ_n \]

Proof ▶

Every point is positive.

Lemma 2.25

For \(r, s \in \mathbb {N}\), one has

\[ J_rs = \int _{0}^{1}\int _{0}^{1}\int _{0}^{1} \frac{y^rz^s}{1-(1-yz)x} \, dz \, dy \, dx \]

Proof ▶

\begin{align*} & \int _{0}^{1}\int _{0}^{1}\int _{0}^{1} \frac{y^rz^s}{1-(1-yz)x} \, dz \, dy \, dx \\ =& \int _{0}^{1}\int _{0}^{1}(\int _{0}^{1} \frac{y^rz^s}{1-(1-yz)x} \, dx) \, dy \, dz \\ =& \int _{0}^{1}\int _{0}^{1}(-\frac{{\rm ln}(yz)}{1 - yz}y^rz^s \, dx) \, dy \, dz \\ =& J_rs \end{align*}

Theorem 2.26

\[ JJ_n \leqslant (\frac{1}{24})^n\cdot 2\zeta (3) \]

Proof ▶

\begin{align*} JJ_n & = JJ’_n \\ & \leqslant (\frac{1}{24})^n \int _{0}^{1}\int _{0}^{1}\int _{0}^{1} \frac{1}{1-(1-yz)x} \, dx \, dy \, dz \\ & = (\frac{1}{24})^n J_{00} \\ & = (\frac{1}{24})^n \cdot 2\zeta (3) \end{align*}

Lemma 2.27

One has

\[ \pi (x) = \left(1 + o(1)\right)\int _2^{x}\frac{1}{\log x} \mathsf{d} x. \]

as \(x \to \infty \).

Proof ▶

We need a precise description of auxiliary constants involved in \(o(1)\) and “sufficiently large” for the purpose of formalisation, we write down the proof in an excruciatingly detailed manner so that each step could be transcribed to Lean4 with relative ease.

Prime Number Theorem ▶

We want to show that \(\frac{\pi \left(x\right)}{{ \int _{2}^{x}\frac{\mathsf{d}t}{\log t}}}-1\) is \(o\left(1\right)\), that is for every \(\epsilon \), there exists \(M_{\epsilon }\in \mathbb {R}\) such that \(\left|\frac{\pi \left(x\right)}{{ \int _{2}^{x}\frac{\mathsf{d}t}{\log t}}}-1\right|\le \epsilon \). We know that for all \(2\le x\),

\[ \pi \left(x\right)={\frac{1}{\log x}\sum _{p\le \lfloor x\rfloor }\log p+{\int _{2}^{x}\frac{\sum _{p\le \lfloor t\rfloor }\log p}{t\log ^{2}t}}\mathsf{d}t}. \]

We also know that for all \(0{\lt}\epsilon \), there exists a function \(f_{\epsilon }:\mathbb {R}\to \mathbb {R}\) such that \(f_{\epsilon }=o\left(\epsilon \right)\) and \(f\) is integrable on \(\left(2,x\right)\) for all \(2\le x\) and for \(x\) sufficiently large, say \(x{\gt}N_{\epsilon }\ge 2\)

\[ \sum _{p\le \lfloor x\rfloor }\log p=x+xf_{\epsilon }\left(x\right). \]

Hence for all \(0{\lt}\epsilon \), such an \(f\) satisfies: for \(x\) sufficiently large

\[ \pi \left(x\right)=\frac{x+xf_{\epsilon }\left(x\right)}{\log x}+\int _{2}^{N_{\epsilon }}\frac{\sum _{p\le \lfloor x\rfloor }\log p}{t\log ^{2}t}\mathsf{d}t+\int _{N_{\epsilon }}^{x}\frac{t+tf_{\epsilon }\left(t\right)}{t\log ^{2}t}\mathsf{d}t, \]

which simplifies to

\[ \pi \left(x\right)=\left(\frac{x}{\log x}+\int _{N_{\epsilon }}^{x}\frac{\mathsf{d}t}{\log ^{2}t}\right)+\left(\frac{xf_{\epsilon }\left(x\right)}{\log x}+\int _{N_{\epsilon }}^{x}\frac{f_{\epsilon }\left(t\right)}{\log ^{2}t}\mathsf{d}t\right)+\int _{2}^{N_{\epsilon }}\frac{\sum _{p\le \lfloor x\rfloor }\log p}{t\log ^{2}t}\mathsf{d}t. \]

Integration by parts tells us that

\[ \frac{x}{\log x}+\int _{N_{\epsilon }}^{x}\frac{\mathsf{d}t}{\log ^{2}t}=\int _{N_{\epsilon }}^{x}\frac{\mathsf{d}t}{\log t}+\frac{N_{\epsilon }}{\log N_{\epsilon }}=\int _{2}^{x}\frac{\mathsf{d}t}{\log t}+\left(\frac{N_{\epsilon }}{\log N_{\epsilon }}-\int _{2}^{N_{\epsilon }}\frac{\mathsf{d}t}{\log t}\right). \]

Hence

\[ \pi \left(x\right)=\int _{2}^{x}\frac{\mathsf{d}t}{\log t}+\left(\frac{xf_{\epsilon }\left(x\right)}{\log x}+\int _{N_{\epsilon }}^{x}\frac{f_{\epsilon }\left(t\right)}{\log ^{2}t}\mathsf{d}t\right)+C_{\epsilon }, \]

for some constant \(C_{\epsilon }\in \mathbb {R}\).

\[ \frac{\pi \left(x\right)}{\int _{2}^{x}\frac{\mathsf{d}t}{\log t}}-1=\left(\frac{xf_{\epsilon }\left(x\right)}{\log x}+\int _{N_{\epsilon }}^{x}\frac{f_{\epsilon }\left(t\right)}{\log ^{2}t}\mathsf{d}t\right)/\int _{2}^{x}\frac{\mathsf{d}t}{\log t}+\frac{C_{\epsilon }}{\int _{2}^{x}\frac{\mathsf{d}t}{\log t}}. \]

Remember that \(f_{\epsilon }=o\left(\epsilon \right)\), so we know for all \(0{\lt}c\), there exists \(M_{c,\epsilon }\) such that for all \(M_{c,\epsilon }{\lt}x\),\(\left|f_{\epsilon }\left(x\right)\right|\le c\epsilon \). Then for \(2{\lt}M_{c,\epsilon }{\lt}x\), we have

\[ \begin{aligned} \frac{xf_{\epsilon }\left(x\right)}{\log x} & \le \frac{c\epsilon \cdot x}{\log x}\\ \left|\int _{N_{\epsilon }}^{x}\frac{f_{\epsilon }\left(t\right)}{\log ^{2}t}\mathsf{d}t\right| & \le \int _{N_{\epsilon }}^{M_{c,\epsilon }}\left|\frac{f_{\epsilon }\left(t\right)}{\log ^{2}t}\right|\mathsf{d}t+\int _{M_{c,\epsilon }}^{x}\left|\frac{f_{\epsilon }\left(t\right)}{\log ^{2}t}\right|\mathsf{d}t\\ & \le \int _{N_{\epsilon }}^{M_{c,\epsilon }}\frac{\left|f_{\epsilon }\left(t\right)\right|}{\log ^{2}t}\mathsf{d}t+c\epsilon \int _{M_{c,\epsilon }}^{x}\frac{\mathsf{d}t}{\log ^{2}t}\\ & =\int _{N_{\epsilon }}^{M_{c,\epsilon }}\frac{\left|f_{\epsilon }\left(t\right)\right|}{\log ^{2}t}\mathsf{d}t+c\epsilon \left(\int _{M_{c,\epsilon }}^{x}\frac{\mathsf{d}t}{\log t}+\frac{M_{c,\epsilon }}{\log M_{c,\epsilon }}-\frac{x}{\log x}\right), \end{aligned} \]

hence for \(M_{c,\epsilon }{\lt}x\), we have

\[ \begin{aligned} \left|\frac{xf_{\epsilon }\left(x\right)}{\log x}+\int _{N_{\epsilon }}^{x}\frac{f_{\epsilon }\left(t\right)}{\log ^{2}t}\mathsf{d}t\right| & \le \int _{N_{\epsilon }}^{M_{c,\epsilon }}\frac{\left|f_{\epsilon }\left(t\right)\right|}{\log ^{2}t}\mathsf{d}t+c\epsilon \left(\int _{M_{c,\epsilon }}^{x}\frac{\mathsf{d}t}{\log t}+\frac{M_{c,\epsilon }}{\log M_{c,\epsilon }}\right)\\ & =\int _{N_{\epsilon }}^{M_{c,\epsilon }}\frac{\left|f_{\epsilon }\left(t\right)\right|}{\log ^{2}t}\mathsf{d}t+c\epsilon \left(\int _{2}^{x}\frac{\mathsf{d}t}{\log t}+\frac{M_{c,\epsilon }}{\log M_{c,\epsilon }}-\int _{M_{c,\epsilon }}^{2}\frac{\mathsf{d}t}{\log t}\right). \end{aligned} \]

Denote \(D_{c,\epsilon }\) to be \(\int _{N_{\epsilon }}^{M_{c,\epsilon }}\frac{\left|f_{\epsilon }\left(t\right)\right|}{\log ^{2}t}\mathsf{d}t+c\epsilon \frac{M_{c,\epsilon }}{\log M_{c,\epsilon }}-c\epsilon \int _{M_{c,\epsilon }}^{2}\frac{\mathsf{d}t}{\log t}\), we notice

\[ \begin{aligned} \left|\frac{\pi \left(x\right)}{\int _{2}^{x}\frac{\mathsf{d}t}{\log t}}-1\right| & \le \left(c\epsilon \int _{2}^{x}\frac{\mathsf{d}t}{\log t}+D_{c,\epsilon }\right)/\int _{2}^{x}\frac{\mathsf{d}t}{\log t}+\frac{C_{\epsilon }}{\int _{2}^{x}\frac{\mathsf{d}t}{\log t}}\\ & =c\epsilon +\frac{D_{c,\epsilon }}{\int _{2}^{x}\frac{\mathsf{d}t}{\log t}}+\frac{C_{\epsilon }}{\int _{2}^{x}\frac{\mathsf{d}t}{\log t}}. \end{aligned} \]

In particular, there exists a constant \(D\) such that for all \(\max \left(M_{\frac{1}{2},\epsilon },N_{\epsilon }\right){\lt}x\),

\[ \left|\frac{\pi \left(x\right)}{\int _{2}^{x}\frac{\mathsf{d}t}{\log t}}-1\right|\le \frac{\epsilon }{2}+\frac{D}{\int _{2}^{x}\frac{\mathsf{d}t}{\log t}}. \]

We now bound \(\int _2^x\frac{\mathsf{d}t}{\log t}\). Note that \(\int _{2}^{x}\frac{\mathsf{d}t}{\log t}\ge \frac{\left(x-2\right)}{\log x}\). Hence for \(x{\gt}e^{s}\) with \(s{\gt}1\), \(\int _{2}^{x}\frac{\mathsf{d}t}{\log t}\ge \frac{e^{s}-2}{s}\) , consequently \(\frac{D}{\int _{2}^{x}\frac{\mathsf{d}t}{\log t}}\le \frac{sD}{e^{s}-2}\le \frac{sD}{e^{s}}\le \frac{\epsilon }{2}\) for \(s\) sufficiently large, say \(s{\gt}A_{\epsilon }{\gt}1\). Thus for all \(x{\gt}\max \left(M_{\frac{1}{2},\epsilon },N_{\epsilon },e^{A_{\epsilon }}\right)\), \(\left|\frac{\pi \left(x\right)}{\int _{2}^{x}\frac{\mathsf{d}t}{\log t}}-1\right|\le \epsilon \). This proves \(\frac{\pi \left(x\right)}{\int _{2}^{x}\frac{\mathsf{d}t}{\log t}}-1\) is \(o\left(1\right)\) for sufficiently large \(x\).

Lemma 2.28

One has

\[ \pi (x) = (1 + o(1))\frac{x}{\log x} \]

as \(x \rightarrow \infty \).

Proof ▶

Lemma 2.29

Let \(n\) be a positive integer. Define \(\pi (n)\) as the number of primes less than (or equal to) \(n\). Then, \(d_n \leqslant n^{\pi (n)} \sim e^n\).

Proof ▶

use Prime Number Theorem.

Theorem 2.30

\(\zeta (3)\) is irrational.

Proof ▶

\[ 0 \neq |J_n| \leqslant (\frac{1}{30})^n\cdot 2\zeta (3) \]

Then

\[ 0 {\lt} |\frac{a_n}{d_n^3} + b_n\zeta (3)| \leqslant (\frac{1}{30})^n\cdot 2\zeta (3) \]

which means that

\[ 0 {\lt} |a_n + d_n^3 b_n\zeta (3)| \leqslant d_n^3(\frac{1}{30})^n\cdot 2\zeta (3) \]

Since \(d_n \leqslant n^{\pi (n)} \sim e^n\) and \(e^3 {\lt} 21\), we have

\[ 0 {\lt} |a_n + c_n\zeta (3)| {\lt} 21^n (\frac{1}{30})^n\cdot 2\zeta (3) = 2(\frac{7}{10})^n \zeta (3) \]

where\(c_n = d_n^3 b_n\) is integer.
Assume \(\zeta (3) = \frac{p}{q}, (p,q)=1\) and \(p,q{\gt}0\). Then

\[ 0 {\lt} |qa_n + pc_n| {\lt} 2p (\frac{7}{10})^n \]