Large-prime criteria for Sylvester-Schur

TheoremLarge-prime criterion from the Erdős layer bound#✓fully proved

Let \(N\) and \(r\) be natural numbers with \(0 < N\) and \(r \le N\), write \(m\#\) for the product of the primes at most \(m\), and let \(L = \lfloor \log_2 N \rfloor\). Put \(P_1 = r\#\) and \(P_k = \lfloor N^{1/k} \rfloor\#\) for \(k \ge 2\). If

\[r! \cdot \prod_{k=1}^{L} P_k < (N + 1 - r)^r,\]

then \(\binom{N}{r}\) has a prime divisor \(p\) with \(p > r\).

theorem exists_large_prime_dvd_choose_of_factorial_mul_prod_erdos_layers_lt_lower_pow
    {N r : ℕ} (hN : 0 < N) (hrN : r ≤ N)
    (hbound :
      r ! * (∏ j ∈ Finset.range (Nat.log 2 N),
          if j = 0 then primorial r else primorial (Nat.nthRoot (j + 1) N)) <
        (N + 1 - r) ^ r) :
    ∃ p : ℕ, p.Prime ∧ r < p ∧ p ∣ Nat.choose N r

Uses 2 · Used by 1

Proof usesErdős layer bound for binomial coefficients without large prime factors · A prime divisor of \(\binom{N}{r}\) above \(r\) from an upper bound below the lower bound

Used byErdős layer criterion for a large prime in a consecutive block

TheoremLarge-prime criterion from the prime-power layer bound#✓fully proved

Let \(N\) and \(r\) be natural numbers with \(0 < N\) and \(r \le N\), write \(m\#\) for the product of the primes at most \(m\), and let \(L = \lfloor \log_2 N \rfloor\). If

\[r! \cdot \prod_{k=1}^{L} \lfloor N^{1/k} \rfloor\# < (N + 1 - r)^r,\]

then \(\binom{N}{r}\) has a prime divisor \(p\) with \(p > r\).

theorem exists_large_prime_dvd_choose_of_factorial_mul_prod_primorial_nthRoot_lt_lower_pow
    {N r : ℕ} (hN : 0 < N) (hrN : r ≤ N)
    (hbound :
      r ! * (∏ j ∈ Finset.range (Nat.log 2 N), primorial (Nat.nthRoot (j + 1) N)) <
        (N + 1 - r) ^ r) :
    ∃ p : ℕ, p.Prime ∧ r < p ∧ p ∣ Nat.choose N r

Uses 2

Proof usesErdős root-layer bound for binomial coefficients without large prime factors · A prime divisor of \(\binom{N}{r}\) above \(r\) from an upper bound below the lower bound

TheoremCentral-range large-prime criterion from the square-root split bound#✓fully proved

Let \(N\) and \(r\) be natural numbers with \(4 \le r\) and \(2r \le N\), and write \(r\#\) for the product of the primes at most \(r\). If \(r \cdot N^{\lfloor \sqrt{N} \rfloor + 1} \cdot r\# < 4^r\), then \(\binom{N}{r}\) has a prime divisor \(p\) with \(p > r\).

theorem exists_large_prime_dvd_choose_of_mul_top_pow_sqrt_mul_primorial_lt_four_pow
    {N r : ℕ} (hr : 4 ≤ r) (hN : 2 * r ≤ N)
    (hbound : r * (N ^ (Nat.sqrt N + 1) * primorial r) < 4 ^ r) :
    ∃ p : ℕ, p.Prime ∧ r < p ∧ p ∣ Nat.choose N r

Uses 2

Proof usesTruncating the prime factorization of a binomial coefficient · Negating the no-large-prime condition for \(\binom{N}{r}\)

TheoremLarge-prime criterion from the square-root split bound#✓fully proved

Let \(N\) and \(r\) be natural numbers with \(0 < N\) and \(r \le N\), and write \(r\#\) for the product of the primes at most \(r\). If \(r! \cdot N^{\lfloor \sqrt{N} \rfloor + 1} \cdot r\# < (N + 1 - r)^r\), then \(\binom{N}{r}\) has a prime divisor \(p\) with \(p > r\).

theorem exists_large_prime_dvd_choose_of_factorial_mul_top_pow_sqrt_mul_primorial_lt_lower_pow
    {N r : ℕ} (hN : 0 < N) (hrN : r ≤ N)
    (hbound : r ! * (N ^ (Nat.sqrt N + 1) * primorial r) < (N + 1 - r) ^ r) :
    ∃ p : ℕ, p.Prime ∧ r < p ∧ p ∣ Nat.choose N r

Uses 2 · Used by 1

Proof usesTruncating the prime factorization of a binomial coefficient · A prime divisor of \(\binom{N}{r}\) above \(r\) from an upper bound below the lower bound

Used bySquare-root and primorial criterion for a large prime in a consecutive block

TheoremLarge-prime criterion from the prime-counting bound#✓fully proved

Let \(N\) and \(r\) be natural numbers with \(0 < N\) and \(r \le N\), and let \(\pi(r)\) be the number of primes at most \(r\). If \(r! \cdot N^{\pi(r)} < (N + 1 - r)^r\), then \(\binom{N}{r}\) has a prime divisor \(p\) with \(p > r\).

theorem exists_large_prime_dvd_choose_of_factorial_mul_top_pow_primeCounting_lt_lower_pow
    {N r : ℕ} (hN : 0 < N) (hrN : r ≤ N)
    (hbound : r ! * N ^ Nat.primeCounting r < (N + 1 - r) ^ r) :
    ∃ p : ℕ, p.Prime ∧ r < p ∧ p ∣ Nat.choose N r

Uses 2 · Used by 1

Proof usesPrime-counting bound for binomial coefficients without large prime factors · A prime divisor of \(\binom{N}{r}\) above \(r\) from an upper bound below the lower bound

Used byPrime-counting criterion for a large prime in a consecutive block

TheoremLarge-prime criterion from the half-plus-one exponent bound#✓fully proved

Let \(N\) and \(r\) be natural numbers with \(0 < N\) and \(r \le N\). If \(r! \cdot N^{\lfloor r/2 \rfloor + 1} < (N + 1 - r)^r\), then \(\binom{N}{r}\) has a prime divisor \(p\) with \(p > r\).

theorem exists_large_prime_dvd_choose_of_factorial_mul_top_pow_half_add_one_lt_lower_pow
    {N r : ℕ} (hN : 0 < N) (hrN : r ≤ N)
    (hbound : r ! * N ^ (r / 2 + 1) < (N + 1 - r) ^ r) :
    ∃ p : ℕ, p.Prime ∧ r < p ∧ p ∣ Nat.choose N r

Uses 2 · Used by 1

Proof usesHalf-exponent bound for binomial coefficients without large prime factors · A prime divisor of \(\binom{N}{r}\) above \(r\) from an upper bound below the lower bound

Used byHalf-exponent criterion for a large prime in a consecutive block

TheoremLarge-prime criterion from the 3r/8 exponent bound#✓fully proved

Let \(N\) and \(r\) be natural numbers with \(0 < N\), \(38 \le r\) and \(r \le N\). If \(r! \cdot N^{\lfloor 3r/8 \rfloor} < (N + 1 - r)^r\), then \(\binom{N}{r}\) has a prime divisor \(p\) with \(p > r\).

theorem exists_large_prime_dvd_choose_of_factorial_mul_top_pow_three_mul_div_eight_lt_lower_pow
    {N r : ℕ} (hN : 0 < N) (hr : 38 ≤ r) (hrN : r ≤ N)
    (hbound : r ! * N ^ (3 * r / 8) < (N + 1 - r) ^ r) :
    ∃ p : ℕ, p.Prime ∧ r < p ∧ p ∣ Nat.choose N r

Uses 2 · Used by 1

Proof usesThree-eighths exponent bound for binomial coefficients without large prime factors · A prime divisor of \(\binom{N}{r}\) above \(r\) from an upper bound below the lower bound

Used byPower-only large-prime criterion from the 3r/8 exponent bound

TheoremPower-only large-prime criterion from the 3r/8 exponent bound#✓fully proved

Let \(N\) and \(r\) be natural numbers with \(0 < N\), \(38 \le r\) and \(r \le N\). If \(r^r \cdot N^{\lfloor 3r/8 \rfloor} < (N + 1 - r)^r\), then \(\binom{N}{r}\) has a prime divisor \(p\) with \(p > r\).

This follows from the criterion with \(r!\) in place of \(r^r\), since \(r! \le r^r\).

theorem exists_large_prime_dvd_choose_of_self_pow_mul_top_pow_three_mul_div_eight_lt_lower_pow
    {N r : ℕ} (hN : 0 < N) (hr : 38 ≤ r) (hrN : r ≤ N)
    (hbound : r ^ r * N ^ (3 * r / 8) < (N + 1 - r) ^ r) :
    ∃ p : ℕ, p.Prime ∧ r < p ∧ p ∣ Nat.choose N r

Uses 1 · Used by 1

Proof usesLarge-prime criterion from the 3r/8 exponent bound

Used byQuadratic starts give a large prime in a consecutive block

TheoremLarge-prime criterion from the r − 1 exponent bound#✓fully proved

Let \(N\) and \(r\) be natural numbers with \(0 < N\), \(2 \le r\) and \(r \le N\). If \(r! \cdot N^{r-1} < (N + 1 - r)^r\), then \(\binom{N}{r}\) has a prime divisor \(p\) with \(p > r\).

theorem exists_large_prime_dvd_choose_of_factorial_mul_top_pow_sub_one_lt_lower_pow
    {N r : ℕ} (hN : 0 < N) (hr : 2 ≤ r) (hrN : r ≤ N)
    (hbound : r ! * N ^ (r - 1) < (N + 1 - r) ^ r) :
    ∃ p : ℕ, p.Prime ∧ r < p ∧ p ∣ Nat.choose N r

Uses 2 · Used by 1

Proof usesElementary power bound for binomial coefficients without large prime factors · A prime divisor of \(\binom{N}{r}\) above \(r\) from an upper bound below the lower bound

Used byLarge starts give a large prime in a consecutive block

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.