Prime-counting estimates for Sylvester-Schur

TheoremNegating the no-large-prime condition for \(\binom{N}{r}\)#✓fully proved

Let \(N\) and \(r\) be natural numbers. If it is not the case that every prime dividing \(\binom{N}{r}\) is at most \(r\), then some prime \(p\) with \(r < p\) divides \(\binom{N}{r}\).

theorem exists_large_prime_dvd_choose_of_not_forall_prime_dvd_le {N r : ℕ}
    (hsmall : ¬ ∀ p : ℕ, p.Prime → p ∣ Nat.choose N r → p ≤ r) :
    ∃ p : ℕ, p.Prime ∧ r < p ∧ p ∣ Nat.choose N r

Used by 5

Used byErdős layer criterion, power-of-four form · A numerical criterion for a prime divisor of \(\binom{N}{r}\) above \(r\) when \(N = 2r + i\) · A numerical criterion for a prime divisor of \(\binom{N}{r}\) above \(r\) when \(N \ge 3r\) · Central-range large-prime criterion from the square-root split bound · A prime divisor of \(\binom{N}{r}\) above \(r\) from an upper bound below the lower bound

TheoremA prime divisor of \(\binom{N}{r}\) above \(r\) from an upper bound below the lower bound#✓fully proved

Let \(N\), \(r\) and \(U\) be natural numbers, and let \(m = \max(N + 1 - r, 0)\). Suppose that \(\binom{N}{r} \le U\) whenever every prime dividing \(\binom{N}{r}\) is at most \(r\), and that \(U < m^r / r!\) as rational numbers. Then some prime \(p\) with \(r < p\) divides \(\binom{N}{r}\).

The quotient \(m^r / r!\) is the standard lower bound for \(\binom{N}{r}\).

theorem exists_large_prime_dvd_choose_of_upper_lt_lower {N r U : ℕ}
    (hupper :
      (∀ p : ℕ, p.Prime → p ∣ Nat.choose N r → p ≤ r) → Nat.choose N r ≤ U)
    (hbound : (U : ℚ) < ((N + 1 - r : ℕ) ^ r : ℚ) / (r ! : ℚ)) :
    ∃ p : ℕ, p.Prime ∧ r < p ∧ p ∣ Nat.choose N r

Uses 1 · Used by 8

Proof usesNegating the no-large-prime condition for \(\binom{N}{r}\)

Used byErdős layer criterion, factorial form · Large-prime criterion from the Erdős layer bound · Large-prime criterion from the prime-power layer bound · Large-prime criterion from the square-root split bound · Large-prime criterion from the prime-counting bound · Large-prime criterion from the half-plus-one exponent bound · Large-prime criterion from the 3r/8 exponent bound · Large-prime criterion from the r − 1 exponent bound

TheoremAt most \(r - 1\) primes up to \(r\)#✓fully proved

For every natural number \(r \ge 2\), the number \(\pi(r)\) of primes \(p \le r\) satisfies \(\pi(r) \le r - 1\), since all such primes lie in \(\{2, \dots, r\}\).

theorem primeCounting_le_sub_one {r : ℕ} (hr : 2 ≤ r) :
    Nat.primeCounting r ≤ r - 1

Used by 1

Used byElementary power bound for binomial coefficients without large prime factors

TheoremAt most \(\lfloor r/2 \rfloor + 1\) primes up to \(r\)#✓fully proved

For every natural number \(r\), the number \(\pi(r)\) of primes \(p \le r\) satisfies \(\pi(r) \le \lfloor r/2 \rfloor + 1\).

theorem primeCounting_le_half_add_one (r : ℕ) :
    Nat.primeCounting r ≤ r / 2 + 1

Used by 1

Used byHalf-exponent bound for binomial coefficients without large prime factors

TheoremErdős's \(3r/8\) prime-counting bound#✓fully proved

For every natural number \(r \ge 38\), the number \(\pi(r)\) of primes \(p \le r\) satisfies \(\pi(r) \le \lfloor 3r/8 \rfloor\).

The infinite tail follows from the residue-class estimate modulo \(30\); the range \(38 \le r < 91\) is checked directly.

theorem primeCounting_le_three_mul_div_eight {r : ℕ} (hr : 38 ≤ r) :
    Nat.primeCounting r ≤ 3 * r / 8

Used by 1

Used byThree-eighths exponent bound for binomial coefficients without large prime factors

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.