Large residual estimates for the Sylvester-Schur theorem

• Power bounds for large residual Sylvester-Schur estimates
• Scaled ternary bound for the Sylvester-Schur large residual estimate

LemmaCentral-offset residual bound#✓fully proved

Let \(n\) and \(k\) be natural numbers with \(945 \le n < k\) and \(k + n - 1 < 3n\), and put \(N = k + n - 1\) and \(i = k - n - 1\). For a natural number \(m\) let \(m\#\) denote the product of all primes \(p \le m\), and let \(P_0 = \lfloor N/3 \rfloor\#\) and \(P_j = \lfloor N^{1/(j+1)} \rfloor\#\) for \(j \ge 1\). Then

\[ n \cdot 2^{i} \cdot \prod_{0 \le j < \lfloor \log_2 N \rfloor} P_j < 3^{i} \cdot 4^{n}. \]

lemma second_residual_large_central_offset_bound {n k : ℕ}
    (hn : 945 ≤ n) (hk : n < k) (hcentral : k + n - 1 < 3 * n) :
    n * (2 ^ (k - n - 1) *
      (∏ j ∈ Finset.range (Nat.log 2 (k + n - 1)),
        if j = 0 then primorial ((k + n - 1) / 3)
        else primorial (Nat.nthRoot (j + 1) (k + n - 1)))) <
      3 ^ (k - n - 1) * 4 ^ n

Uses 5 · Used by 1

Proof usesA power comparison for the central-offset estimate · Cube root times logarithm on a linear range · A linear bound by a power of four · Square root bound on a linear range · Three-layer power-of-four bound for the Erdős layer product

Used byErdős key lemma

LemmaTiny-range prime-counting bound#✓fully proved

Let \(n\) and \(k\) be natural numbers with \(7 \le n < 38\) and \(k \ge 100\), and let \(\pi(n)\) be the number of primes \(p \le n\). Then \(n! \cdot (k + n - 1)^{\pi(n)} < k^{n}\).

lemma second_residual_tiny_primeCounting_lt_start_pow {n k : ℕ}
    (hn7 : 7 ≤ n) (hnlt38 : n < 38) (hk100 : 100 ≤ k) :
    Nat.factorial n * (k + n - 1) ^ Nat.primeCounting n < k ^ n

Used by 1

Used byErdős key lemma

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.