6 Applications of explicit PNTs

6.1 Problem statement and notation

Definition 34

\(\sigmafunc (n)\) is the sum of the divisors of \(n\).

Definition 35

A positive integer \(N\) is called highly abundant (HA) if

\[ \sigmafunc (N) {\gt} \sigmafunc (m) \]

for all positive integers \(m {\lt} N\), where \(\sigmafunc (n)\) denotes the sum of the positive divisors of \(n\).

Definition 36

For each integer \(n \ge 1\), define

\[ L_n := \lcm (1,2,\dots ,n). \]

We call \((L_n)_{n \ge 1}\) the least common multiple sequence.

Definition 37

We say that \(L_n\) is highly abundant if \(L_n\) is a highly abundant integer in the sense above, i.e.

\[ \sigmafunc (L_n) {\gt} \sigmafunc (m) \quad \text{for all } m {\lt} L_n. \]

Original MathOverflow question. Is it true that every value in the sequence \(L_n = \lcm (1,2,\dots ,n)\) is highly abundant? Equivalently,
\[ \{ L_n : n \ge 1\} \subseteq HA? \]

In this note we record the structure of an argument showing that, for all sufficiently large \(n\), the integer \(L_n\) is not highly abundant. This argument was taken from this MathOverflow answer.

6.2 A general criterion using three medium primes and three large primes

The goal of this section is to prove:

Theorem 49

Let \(n \geq 1\). Suppose that primes \(p_1,p_2,p_3,q_1,q_2,q_3\) satisfy

\[ \sqrt{n} {\lt} p_1 {\lt} p_2 {\lt} p_3 {\lt} q_1 {\lt} q_2 {\lt} q_3 {\lt} n \]

and the key criterion

\begin{equation} \label{eq:main-ineq} \prod _{i=1}^3\Bigl(1+\frac{1}{q_i}\Bigr) \le \Biggl( \prod _{i=1}^3 \Bigl(1+\frac{1}{p_i(p_i+1)}\Bigr) \Biggr) \Bigl(1 + \frac{3}{8n}\Bigr) \Biggl(1 - \frac{4 p_1 p_2 p_3}{q_1 q_2 q_3}\Biggr). \end{equation}

Then \(L_n\) is not highly abundant.

In the rest of the section we assume the hypotheses of Theorem 49.

Lemma 128

We have \(4 p_1 p_2 p_3 {\lt} q_1 q_2 q_3\).

Proof ▶

Obvious from the non-negativity of the left-hand side of 1.

6.2.1 Factorisation of \(L_n\) and construction of a competitor

Lemma 129 Factorisation of \(L_n\)

There exists a positive integer \(L'\) such that

\[ L_n = q_1 q_2 q_3 \, L' \]

and each prime \(q_i\) divides \(L_n\) exactly once and does not divide \(L'\).

Proof ▶

Since \(q_i {\lt} n\), the prime \(q_i\) divides \(L_n\) exactly once (as \(q_i^2 {\gt} n\)). Hence we may write \(L_n = q_1 q_2 q_3 L'\) where \(L'\) is the quotient obtained by removing these prime factors. By construction, \(q_i \nmid L'\) for each \(i\).

Lemma 130 Normalised divisor sum for \(L_n\)

Let \(L'\) be as in Lemma 129. Then

\begin{equation} \label{eq:sigmaLn} \frac{\sigmafunc (L_n)}{L_n} \; =\; \frac{\sigmafunc (L')}{L'} \prod _{i=1}^3 \Bigl(1 + \frac{1}{q_i}\Bigr). \end{equation}

Proof ▶

Use the multiplicativity of \(\sigmafunc (\cdot )\) and the fact that each \(q_i\) occurs to the first power in \(L_n\). Then

\[ \sigmafunc (L_n) = \sigmafunc (L') \prod _{i=1}^3 \sigmafunc (q_i) = \sigmafunc (L') \prod _{i=1}^3 (1+q_i). \]

Dividing by \(L_n = L' \prod _{i=1}^3 q_i\) gives

\[ \frac{\sigmafunc (L_n)}{L_n} = \frac{\sigmafunc (L')}{L'} \prod _{i=1}^3 \frac{1+q_i}{q_i} = \frac{\sigmafunc (L')}{L'} \prod _{i=1}^3 \Bigl(1 + \frac{1}{q_i}\Bigr). \]

Lemma 131

There exist integers \(m \ge 0\) and \(r\) satisfying \(0 {\lt} r {\lt} 4 p_1 p_2 p_3\) and

\[ q_1 q_2 q_3 = 4 p_1 p_2 p_3 m + r \]

Proof ▶

This is division with remainder.

Definition 38

With \(m,r\) as above, define the competitor

\[ M := 4 p_1 p_2 p_3 m L'. \]

Lemma 132 Basic properties of \(M\)

With notation as above, we have:

\(0 {\lt} r {\lt} 4 p_1 p_2 p_3\).
\(M {\lt} L_n\).
\[ 1 {\lt} \frac{L_n}{M} = \Bigl(1 - \frac{r}{q_1 q_2 q_3}\Bigr)^{-1} {\lt} \Bigl(1 - \frac{4 p_1 p_2 p_3}{q_1 q_2 q_3}\Bigr)^{-1}. \]

Proof ▶

The first item is by construction of the division algorithm. For the second, note that

\[ L_n = q_1 q_2 q_3 L' = (4 p_1 p_2 p_3 m + r) L' {\gt} 4 p_1 p_2 p_3 m L' = M, \]

since \(r{\gt}0\). For the third,

\[ \frac{L_n}{M} = \frac{4 p_1 p_2 p_3 m + r}{4 p_1 p_2 p_3 m} = 1 + \frac{r}{4 p_1 p_2 p_3 m} = \Bigl(1 - \frac{r}{4 p_1 p_2 p_3 m + r}\Bigr)^{-1} = \Bigl(1 - \frac{r}{q_1 q_2 q_3}\Bigr)^{-1}. \]

Since \(0 {\lt} r {\lt} 4p_1p_2p_3\) and \(4p_1p_2p_3 {\lt} q_1q_2q_3\), we have

\[ 0{\lt}\frac{r}{q_1 q_2 q_3}{\lt}\frac{4p_1p_2p_3}{q_1 q_2 q_3}, \]

\[ \Bigl(1-\frac{r}{q_1 q_2 q_3}\Bigr)^{-1} {\lt} \Bigl(1-\frac{4p_1p_2p_3}{q_1 q_2 q_3}\Bigr)^{-1}. \]

6.2.2 A sufficient condition

We give a sufficient condition for \(\sigmafunc (M) \geq \sigmafunc (L_n)\).

Lemma 133 A sufficient inequality

Suppose

\[ \frac{\sigmafunc (M)}{M} \Bigl(1 - \frac{4 p_1 p_2 p_3}{q_1 q_2 q_3}\Bigr) \; \ge \; \frac{\sigmafunc (L_n)}{L_n}. \]

Then \(\sigmafunc (M) \ge \sigmafunc (L_n)\).

Proof ▶

By Lemma 132,

\[ \frac{L_n}{M} {\lt} \Bigl(1 - \frac{4 p_1 p_2 p_3}{q_1 q_2 q_3}\Bigr)^{-1}. \]

Hence

\[ \frac{\sigmafunc (M)}{M} \ge \frac{\sigmafunc (L_n)}{L_n} \Bigl(1 - \frac{4 p_1 p_2 p_3}{q_1 q_2 q_3}\Bigr)^{-1} {\gt} \frac{\sigmafunc (L_n)}{L_n} \cdot \frac{M}{L_n}. \]

Multiplying both sides by \(M\) gives

\[ \sigmafunc (M) {\gt} \sigmafunc (L_n) \cdot \frac{M}{L_n} \]

and hence

\[ \sigmafunc (M) \ge \sigmafunc (L_n), \]

since \(M/L_n{\lt}1\) and both sides are integers.

Combining Lemma 133 with Lemma 130, we see that it suffices to bound \(\sigmafunc (M)/M\) from below in terms of \(\sigmafunc (L')/L'\):

Lemma 134 Reduction to a lower bound for \(\sigmafunc (M)/M\)

\begin{equation} \label{eq:sigmaM-lower} \frac{\sigmafunc (M)}{M} \; \ge \; \frac{\sigmafunc (L')}{L'} \Biggl( \prod _{i=1}^3 \Bigl(1+\frac{1}{p_i(p_i+1)}\Bigr) \Biggr) \Bigl(1 + \frac{3}{8n}\Bigr), \end{equation}

then

\[ \frac{\sigmafunc (M)}{M} \Bigl(1 - \frac{4 p_1 p_2 p_3}{q_1 q_2 q_3}\Bigr) \ge \frac{\sigmafunc (L_n)}{L_n}. \]

Proof ▶

Insert 3 and 2 into the desired inequality and compare with the assumed bound 1; this is a straightforward rearrangement.

6.2.3 Effect of modifying prime powers

Now we estimate the effect on \(\sigmafunc (\cdot )/(\cdot )\) of increasing certain prime exponents.

Lemma 135 Effect of increasing the exponent of \(p_i\)

Fix \(i \in \{ 1,2,3\} \). Suppose that in passing from \(L'\) to \(M\) we increase the exponent of \(p_i\) by exactly \(1\). Then the normalised divisor sum is multiplied by a factor

\[ \frac{(1+p_i+p_i^2)/p_i^2}{(1+p_i)/p_i} = 1 + \frac{1}{p_i(p_i+1)}. \]

Proof ▶

If the exponent of \(p_i\) in \(L'\) is \(e\), the contribution of \(p_i\) to \(\sigmafunc (L')/L'\) is

\[ \frac{1 + p_i + \dots + p_i^e}{p_i^e}. \]

Increasing the exponent to \(e+1\) multiplies this factor by

\[ \frac{(1+p_i+\dots +p_i^{e+1})/p_i^{e+1}}{(1+p_i+\dots +p_i^e)/p_i^e} = \frac{1+p_i+\dots +p_i^{e+1}}{p_i(1+p_i+\dots +p_i^e)} = \frac{1+p_i+\dots +p_i^e + p_i^{e+1}}{p_i(1+p_i+\dots +p_i^e)}. \]

Since all terms \(1,p_i,\dots \) are positive, replacing \(e\) by \(1\) only decreases this ratio. Thus

\[ \frac{(1+p_i+p_i^2)/p_i^2}{(1+p_i)/p_i} \le \frac{(1+p_i+\dots +p_i^{e+1})/p_i^{e+1}}{(1+p_i+\dots +p_i^e)/p_i^e}. \]

In our application, the exponent is exactly increased by \(1\), and we may bound from below by the case \(e=1\), giving the claimed factor

\[ 1 + \frac{1}{p_i(p_i+1)}. \]

Lemma 136 Effect of increasing the exponent of \(2\)

Let \(k\) be the largest integer such that \(2^k \le n\). Then the exponent of \(2\) in \(L'\) is at least \(k\), and the exponent of \(2\) in \(M\) is at least \(k+2\). Consequently,

\begin{equation} \label{eq:2-lower} \frac{(1+2+\dots +2^{k+2})/2^{k+2}}{(1+2+\dots +2^k)/2^k} \ge 1 + \frac{3}{2^{k+3}-4} \ge 1 + \frac{3}{8n}. \end{equation}

Proof ▶

Since \(2^k \le n\), the number \(2^k\) divides \(\lcm (1,2,\dots ,n)\), hence \(2^k\) divides \(L_n\) and thus also divides \(L'\). The definition of \(M\) multiplies \(L'\) by \(4 = 2^2\), so the exponent of \(2\) in \(M\) is at least \(k+2\).

The ratio of contributions of \(2\) to \(\sigmafunc (M)/M\) and \(\sigmafunc (L')/L'\) is

\[ \frac{(1+2+\dots +2^{k+2})/2^{k+2}}{(1+2+\dots +2^k)/2^k}. \]

A direct calculation yields

\[ \frac{1+2+\dots +2^{k+2}}{1+2+\dots +2^k} = \frac{2^{k+3}-1}{2^{k+1}-1} = 1 + \frac{3(2^k-1)}{2^{k+1}-1} \ge 1 + \frac{3}{2^{k+3}-4}, \]

giving the first inequality in 4. Finally, since \(2^k \le n {\lt} 2^{k+1}\), we have \(2^{k+3} {\lt} 8n\), so

\[ \frac{3}{2^{k+3}-4} \ge \frac{3}{8n}, \]

giving the second inequality.

Lemma 137 Effect of the remaining factor \(m\)

The extra factor \(m\) in the definition of \(M\) can only increase the normalised divisor sum:

\[ \frac{\sigmafunc (M)}{M} \ge \frac{\sigmafunc (L')}{L'} \times \Bigl(\text{multiplicative factors coming from }p_i\text{ and }2\Bigr). \]

Proof ▶

Since \(m\) is a positive integer, any extra primes (or higher exponents) it introduces appear as multiplicative factors of the form

\[ \frac{1+p+\dots +p^e}{p^e} \ge 1. \]

Hence they can only increase the value of \(\sigmafunc (M)/M\).

6.2.4 Conclusion of the criterion

Lemma 138 Lower bound for \(\sigmafunc (M)/M\)

With notation as above,

\[ \frac{\sigmafunc (M)}{M} \ge \frac{\sigmafunc (L')}{L'} \Biggl( \prod _{i=1}^3 \Bigl(1 + \frac{1}{p_i(p_i+1)}\Bigr) \Biggr) \Bigl(1 + \frac{3}{8n}\Bigr). \]

Proof ▶

Multiply the contributions from Lemma 135 for \(i=1,2,3\), from Lemma 136 for the prime \(2\), and note that Lemma 137 allows us to ignore any additional (non-decreasing) contribution from \(m\). This gives exactly the stated lower bound.

Proof of Theorem 49 ▶

By Lemma 138, the condition 3 holds. By Lemma 134 this implies

\[ \frac{\sigmafunc (M)}{M} \Bigl(1 - \frac{4 p_1 p_2 p_3}{q_1 q_2 q_3}\Bigr) \ge \frac{\sigmafunc (L_n)}{L_n}. \]

Applying Lemma 133, we obtain \(\sigmafunc (M) \ge \sigmafunc (L_n)\) with \(M {\lt} L_n\), so \(L_n\) cannot be highly abundant.

Analogous arguments allow other pairs \((c,\alpha )\) in place of \((4,3/8)\), such as \((2,1/4)\), \((6,17/36)\), \((30,0.632\dots )\); or even \((1,0)\) provided more primes are used on the \(p\)-side than the \(q\)-side to restore an asymptotic advantage.

6.3 Asymptotic selection of primes using Dusart’s result

In this section we use explicit prime gap estimates to show that the hypotheses of Theorem 49 hold for all sufficiently large \(n\).

6.3.1 An explicit prime gap result (Dusart)

Theorem 50 Dusart

There exists a constant \(X_0\) (one may take \(X_0 = 89693\)) with the following property: for every real \(x \ge X_0\), there exists a prime \(p\) with

\[ x {\lt} p \le x\Bigl(1 + \frac{1}{\log ^3 x}\Bigr). \]

In the Lean formalization, Theorem 50 will be taken as an axiom or imported lemma, without re-proving it.

6.3.2 Choice of six primes \(p_i,q_i\) for large \(n\)

Lemma 139 Choice of medium primes \(p_i\)

Let \(n \ge X_0^2\). Set \(x := \sqrt{n}\). Then, by repeated application of Theorem 50, there exist primes \(p_1,p_2,p_3\) with

\[ p_i \le x \Bigl(1 + \frac{1}{\log ^3 x}\Bigr)^i \]

and \(p_1 {\lt} p_2 {\lt} p_3\). Moreover, \(\sqrt{n} {\lt} p_1\) (for \(n\) sufficiently large).

Proof ▶

Apply Theorem 50 successively with \(x, x(1+1/\log ^3 x), x(1+1/\log ^3 x)^2\), keeping track of the resulting primes and bounds. For \(n\) large and \(x = \sqrt{n}\), we have \(\sqrt{n} {\lt} p_1\) as soon as the first interval lies strictly above \(\sqrt{n}\); this can be enforced by taking \(n\) large enough.

Lemma 140 Choice of large primes \(q_i\)

Let \(n \ge X_0^2\). Then there exist primes \(q_1 {\lt} q_2 {\lt} q_3\) with

\[ q_{4-i} \ge n \Bigl(1 + \frac{1}{\log ^3 \sqrt{n}}\Bigr)^{-i} \]

for \(i = 1,2,3\), and \(q_1 {\lt} q_2 {\lt} q_3 {\lt} n\).

Proof ▶

Apply Theorem 50 with suitable values of \(x\) slightly below \(n\), e.g. \(x = n(1+1/\log ^3\sqrt{n})^{-i}\), again keeping track of the intervals. For \(n\) large enough, these intervals lie in \((\sqrt{n},n)\) and contain primes \(q_i\) with the desired ordering.

6.3.3 Bounding the factors in 1

Lemma 141 Bounds for the \(q_i\)-product

With \(p_i,q_i\) as in Lemmas 139 and 140, we have

\begin{equation} \label{eq:qi-upper} \prod _{i=1}^3 \Bigl(1 + \frac{1}{q_i}\Bigr) \le \prod _{i=1}^3 \Bigl(1 + \frac{\bigl(1 + \frac{1}{\log ^3 \sqrt{n}}\bigr)^i}{n} \Bigr). \end{equation}

Proof ▶

By Lemma 140, each \(q_i\) is at least

\[ n\Bigl(1 + \frac{1}{\log ^3 \sqrt{n}}\Bigr)^{-j} \]

for suitable indices \(j\), so \(1/q_i\) is bounded above by

\[ \frac{\bigl(1 + \frac{1}{\log ^3 \sqrt{n}}\bigr)^i}{n} \]

after reindexing. Multiplying the three inequalities gives 5.

Lemma 142 Bounds for the \(p_i\)-product

With \(p_i\) as in Lemma 139, we have for large \(n\)

\begin{equation} \label{eq:pi-lower} \prod _{i=1}^3 \Bigl(1 + \frac{1}{p_i(p_i+1)}\Bigr) \ge \prod _{i=1}^3 \Bigl( 1 + \frac{1}{\bigl(1 + \frac{1}{\log ^3 \sqrt{n}}\bigr)^{2i} (n + \sqrt{n})} \Bigr). \end{equation}

Proof ▶

By Lemma 139, \(p_i \le \sqrt{n} (1+1/\log ^3\sqrt{n})^i\). Hence

\[ p_i^2 \le n\bigl(1 + \tfrac {1}{\log ^3 \sqrt{n}}\bigr)^{2i} \quad \text{and}\quad p_i+1 \le p_i(1 + 1/\sqrt{n}) \le (1+1/\sqrt{n}) p_i. \]

From these one gets

\[ p_i(p_i+1) \le \bigl(1 + \tfrac {1}{\log ^3 \sqrt{n}}\bigr)^{2i} (n + \sqrt{n}), \]

and hence

\[ \frac{1}{p_i(p_i+1)} \ge \frac{1}{\bigl(1 + \tfrac {1}{\log ^3 \sqrt{n}}\bigr)^{2i} (n + \sqrt{n})}. \]

Taking \(1+\cdot \) and multiplying over \(i=1,2,3\) gives 6.

Lemma 143 Lower bound for the product ratio \(p_i/q_i\)

With \(p_i,q_i\) as in Lemmas 139 and 140, we have

\begin{equation} \label{eq:pq-ratio} 1 - \frac{4 p_1 p_2 p_3}{q_1 q_2 q_3} \ge 1 - \frac{4 \bigl(1 + \frac{1}{\log ^3 \sqrt{n}}\bigr)^{12}}{n^{3/2}}. \end{equation}

Proof ▶

We have \(p_i \le \sqrt{n} (1+1/\log ^3 \sqrt{n})^i\), so

\[ p_1 p_2 p_3 \le n^{3/2} \bigl(1 + \tfrac {1}{\log ^3 \sqrt{n}}\bigr)^{6}. \]

Similarly, \(q_i \ge n(1+1/\log ^3 \sqrt{n})^{-i}\), so

\[ q_1 q_2 q_3 \ge n^3 \bigl(1 + \tfrac {1}{\log ^3 \sqrt{n}}\bigr)^{-6}. \]

Combining,

\[ \frac{p_1 p_2 p_3}{q_1 q_2 q_3} \le \frac{n^{3/2} \bigl(1 + \frac{1}{\log ^3 \sqrt{n}}\bigr)^{6}}{n^3 \bigl(1 + \frac{1}{\log ^3 \sqrt{n}}\bigr)^{-6}} = \frac{\bigl(1 + \frac{1}{\log ^3 \sqrt{n}}\bigr)^{12}}{n^{3/2}}. \]

This implies 7.

6.3.4 Reduction to a small epsilon-inequality

Lemma 144 Uniform bounds for large \(n\)

For all \(n \ge X_0^2 = 89693^2\) we have

\[ \frac{1}{\log ^3 \sqrt{n}} \le 0.000675, \qquad \frac{1}{n^{3/2}} \le \frac{1}{89693}\cdot \frac{1}{n}. \]

Proof ▶

This is a straightforward calculus and monotonicity check: the left-hand sides are decreasing in \(n\) for \(n \ge X_0^2\), and equality (or the claimed upper bound) holds at \(n=X_0^2\). One can verify numerically or symbolically.

Definition 39

For \(n \ge X_0^2\), define \(\varepsilon := 1/n\). Then

\[ 0 {\lt} \varepsilon \le \frac{1}{X_0^2} = \frac{1}{89693^2}. \]

Lemma 145 Polynomial approximation of the inequality

For \(0 \le \varepsilon \le 1/89693^2\), we have

\[ \prod _{i=1}^3 (1 + 1.000675^i \varepsilon ) \le \Bigl(1 + 3.01\varepsilon + 3.01\varepsilon ^2 + 1.01\varepsilon ^3\Bigr), \]

and

\[ \prod _{i=1}^3 \Bigl(1 + \frac{\varepsilon }{1.000675^{2i}}\Bigr) \Bigl(1 + \frac{3}{8}\varepsilon \Bigr) \Bigl(1 - \frac{4 \times 1.000675^{12}}{89693}\varepsilon \Bigr) \ge 1 + 3.37\varepsilon - 0.01\varepsilon ^2. \]

Proof ▶

Expand each finite product as a polynomial in \(\varepsilon \), estimate the coefficients using the bounds in Lemma 144, and bound the tails by simple inequalities such as

\[ (1+C\varepsilon )^k \le 1 + k C\varepsilon + \dots \]

for small \(\varepsilon \). All coefficients can be bounded numerically in a rigorous way; this step is a finite computation that can be checked mechanically.

Lemma 146 Final polynomial comparison

For \(0 \le \varepsilon \le 1/89693^2\), we have

\[ 1 + 3.01\varepsilon + 3.01\varepsilon ^2 + 1.01\varepsilon ^3 \le 1 + 3.37\varepsilon - 0.01\varepsilon ^2. \]

Proof ▶

This is equivalent to

\[ 3.01\varepsilon + 3.01\varepsilon ^2 + 1.01\varepsilon ^3 \le 3.37\varepsilon - 0.01\varepsilon ^2, \]

\[ 0 \le (3.37 - 3.01)\varepsilon - (3.01+0.01)\varepsilon ^2 - 1.01\varepsilon ^3. \]

Factor out \(\varepsilon \) and use that \(0{\lt}\varepsilon \le 1/89693^2\) to check that the resulting quadratic in \(\varepsilon \) is nonnegative on this interval. Again, this is a finite computation that can be verified mechanically.

Proposition 8 Verification of 1 for large \(n\)

For every integer \(n \ge X_0^2 = 89693^2 \approx 8.04\times 10^9\), the primes \(p_i,q_i\) constructed in Lemmas 139 and 140 satisfy the inequality 1.

Proof ▶

Combine Lemma 141, Lemma 142, and Lemma 143. Then apply Lemma 144 and set \(\varepsilon = 1/n\). The products are bounded by the expressions in Lemma 145, and the inequality in Lemma 146 then ensures that 1 holds.

6.3.5 Conclusion for large \(n\)

Theorem 51 Non-highly abundant for large \(n\)

For every integer \(n \ge 89693^2\), the integer \(L_n\) is not highly abundant.

Proof ▶

By Proposition 8, there exist primes \(p_1,p_2,p_3,q_1,q_2,q_3\) satisfying the hypotheses of Theorem 49. Hence \(L_n\) is not highly abundant.

In combination with earlier arguments and computations for smaller \(n\), one can conclude that \(L_n\) is highly abundant only for finitely many indices \(n\), and these indices can be determined explicitly by exhaustive computation.