Power-of-four bounds for Sylvester-Schur

TheoremCentral Erdős layer estimate#✓fully proved

Let \(n \ge 512\) be a natural number and \(N = 2n + 2\). For a natural number \(x\) write \(x\#\) for the primorial of \(x\), the product of all primes \(p \le x\), and let \(L = \lfloor \log_2 N \rfloor\). Then \(n \cdot \lfloor N/3 \rfloor\# \cdot \prod_{m=2}^{L} \lfloor N^{1/m} \rfloor\# < 4^n\).

theorem central_erdos_layers_two_mul_add_two_lt_four_pow {n : ℕ} (hn : 512 ≤ n) :
    n * (∏ j ∈ Finset.range (Nat.log 2 (2 * n + 2)),
        if j = 0 then primorial ((2 * n + 2) / 3)
        else primorial (Nat.nthRoot (j + 1) (2 * n + 2))) < 4 ^ n

Used by 1

Used byErdős key lemma

TheoremPower-of-four bound for the Erdős layer product#✓fully proved

Let \(N\) and \(r\) be natural numbers. For a natural number \(x\) write \(x\#\) for the primorial of \(x\), the product of all primes \(p \le x\). Let \(L = \lfloor \log_2 N \rfloor\), with \(L = 0\) when \(N = 0\), and let \(P = 1\) if \(L = 0\) and \(P = r\# \cdot \prod_{m=2}^{L} \lfloor N^{1/m} \rfloor\#\) if \(L \ge 1\). Then \(P \le 4^{r + \lfloor \sqrt{N} \rfloor L}\).

This is a coarse bound, weaker than the full Erdős estimate, but much sharper than replacing the first layer by \(\lfloor N/3 \rfloor\) when \(N\) is several multiples of \(r\).

theorem erdos_layers_le_four_pow (N r : ℕ) :
    (∏ j ∈ Finset.range (Nat.log 2 N),
        if j = 0 then primorial r else primorial (Nat.nthRoot (j + 1) N)) ≤
      4 ^ (r + Nat.sqrt N * Nat.log 2 N)

Used by 1

Used bySylvester–Schur criterion from the coarse power-of-four Erdős bound

TheoremThree-layer power-of-four bound for the Erdős layer product#✓fully proved

Let \(N\) and \(r\) be natural numbers. For a natural number \(x\) write \(x\#\) for the primorial of \(x\), the product of all primes \(p \le x\). Let \(L = \lfloor \log_2 N \rfloor\), with \(L = 0\) when \(N = 0\), and let \(P = 1\) if \(L = 0\) and \(P = r\# \cdot \prod_{m=2}^{L} \lfloor N^{1/m} \rfloor\#\) if \(L \ge 1\). Then \(P \le 4^{r + \lfloor \sqrt{N} \rfloor + \lfloor N^{1/3} \rfloor L}\).

The first layer contributes \(r\), the second \(\lfloor \sqrt{N} \rfloor\), and all remaining layers are controlled by the cube root of \(N\). This is the reusable form of the estimate used in Erdős's case split.

theorem erdos_layers_le_four_pow_three_layers (N r : ℕ) :
    (∏ j ∈ Finset.range (Nat.log 2 N),
        if j = 0 then primorial r else primorial (Nat.nthRoot (j + 1) N)) ≤
      4 ^ (r + Nat.sqrt N + Nat.nthRoot 3 N * Nat.log 2 N)

Used by 3

Used bySylvester–Schur criterion from the three-layer power-of-four Erdős bound · A numerical criterion for a prime divisor of \(\binom{N}{r}\) above \(r\) when \(N \ge 3r\) · Central-offset residual bound

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.