Binomial factorization bounds for Sylvester-Schur

TheoremTruncating the prime factorization of a binomial coefficient#✓fully proved

Let \(r \le N\) be natural numbers such that every prime divisor of \(\binom{N}{r}\) is at most \(r\). Then \(\prod_{p=0}^{r} p^{v_p(\binom{N}{r})} = \binom{N}{r}\), where \(v_p(m)\) is the exponent of \(p\) in the prime factorization of \(m\) (zero when \(p\) is not prime).

theorem choose_eq_prod_small_prime_powers_of_no_large {N r : ℕ} (hrN : r ≤ N)
    (hsmall : ∀ p : ℕ, p.Prime → p ∣ Nat.choose N r → p ≤ r) :
    (∏ p ∈ Finset.range (r + 1), p ^ (Nat.choose N r).factorization p) =
      Nat.choose N r

Used by 6

Used byErdős layer bound with a one-third first layer · Erdős layer bound for binomial coefficients without large prime factors · Erdős root-layer bound for binomial coefficients without large prime factors · Prime-counting bound for binomial coefficients without large prime factors · Large-prime criterion from the square-root split bound · Central-range large-prime criterion from the square-root split bound

TheoremPrime-counting bound for binomial coefficients without large prime factors#✓fully proved

Let \(0 < N\) and \(r \le N\) be natural numbers such that every prime divisor of \(\binom{N}{r}\) is at most \(r\). Then \(\binom{N}{r} \le N^{\pi(r)}\), where \(\pi(r)\) is the number of primes \(p \le r\).

theorem choose_le_top_pow_primeCounting_of_no_large {N r : ℕ} (hN : 0 < N) (hrN : r ≤ N)
    (hsmall : ∀ p : ℕ, p.Prime → p ∣ Nat.choose N r → p ≤ r) :
    Nat.choose N r ≤ N ^ Nat.primeCounting r

Uses 1 · Used by 4

Proof usesTruncating the prime factorization of a binomial coefficient

Used byHalf-exponent bound for binomial coefficients without large prime factors · Elementary power bound for binomial coefficients without large prime factors · Three-eighths exponent bound for binomial coefficients without large prime factors · Large-prime criterion from the prime-counting bound

TheoremElementary power bound for binomial coefficients without large prime factors#✓fully proved

Let \(0 < N\) and \(2 \le r \le N\) be natural numbers such that every prime divisor of \(\binom{N}{r}\) is at most \(r\). Then \(\binom{N}{r} \le N^{r-1}\).

theorem choose_le_top_pow_sub_one_of_no_large {N r : ℕ} (hN : 0 < N) (hr : 2 ≤ r)
    (hrN : r ≤ N) (hsmall : ∀ p : ℕ, p.Prime → p ∣ Nat.choose N r → p ≤ r) :
    Nat.choose N r ≤ N ^ (r - 1)

Uses 2 · Used by 1

Proof usesPrime-counting bound for binomial coefficients without large prime factors · At most \(r - 1\) primes up to \(r\)

Used byLarge-prime criterion from the r − 1 exponent bound

TheoremHalf-exponent bound for binomial coefficients without large prime factors#✓fully proved

Let \(0 < N\) and \(r \le N\) be natural numbers such that every prime divisor of \(\binom{N}{r}\) is at most \(r\). Then \(\binom{N}{r} \le N^{\lfloor r/2 \rfloor + 1}\).

theorem choose_le_top_pow_half_add_one_of_no_large {N r : ℕ} (hN : 0 < N) (hrN : r ≤ N)
    (hsmall : ∀ p : ℕ, p.Prime → p ∣ Nat.choose N r → p ≤ r) :
    Nat.choose N r ≤ N ^ (r / 2 + 1)

Uses 2 · Used by 1

Proof usesPrime-counting bound for binomial coefficients without large prime factors · At most \(\lfloor r/2 \rfloor + 1\) primes up to \(r\)

Used byLarge-prime criterion from the half-plus-one exponent bound

TheoremThree-eighths exponent bound for binomial coefficients without large prime factors#✓fully proved

Let \(0 < N\) and \(38 \le r \le N\) be natural numbers such that every prime divisor of \(\binom{N}{r}\) is at most \(r\). Then \(\binom{N}{r} \le N^{\lfloor 3r/8 \rfloor}\).

theorem choose_le_top_pow_three_mul_div_eight_of_no_large {N r : ℕ} (hN : 0 < N)
    (hr : 38 ≤ r) (hrN : r ≤ N)
    (hsmall : ∀ p : ℕ, p.Prime → p ∣ Nat.choose N r → p ≤ r) :
    Nat.choose N r ≤ N ^ (3 * r / 8)

Uses 2 · Used by 1

Proof usesPrime-counting bound for binomial coefficients without large prime factors · Erdős's \(3r/8\) prime-counting bound

Used byLarge-prime criterion from the 3r/8 exponent bound

TheoremErdős root-layer bound for binomial coefficients without large prime factors#✓fully proved

Let \(0 < N\) and \(r \le N\) be natural numbers such that every prime divisor of \(\binom{N}{r}\) is at most \(r\). Write \(P(m)\) for the product of all primes \(p \le m\) and let \(L = \lfloor \log_2 N \rfloor\). Then \(\binom{N}{r} \le \prod_{k=1}^{L} P(\lfloor N^{1/k} \rfloor)\).

theorem choose_le_prod_primorial_nthRoot_of_no_large {N r : ℕ} (hN : 0 < N)
    (hrN : r ≤ N) (hsmall : ∀ p : ℕ, p.Prime → p ∣ Nat.choose N r → p ≤ r) :
    Nat.choose N r ≤
      ∏ j ∈ Finset.range (Nat.log 2 N), primorial (Nat.nthRoot (j + 1) N)

Uses 1 · Used by 1

Proof usesTruncating the prime factorization of a binomial coefficient

Used byLarge-prime criterion from the prime-power layer bound

TheoremErdős layer bound for binomial coefficients without large prime factors#✓fully proved

Let \(0 < N\) and \(r \le N\) be natural numbers such that every prime divisor of \(\binom{N}{r}\) is at most \(r\). Write \(P(m)\) for the product of all primes \(p \le m\) and let \(L = \lfloor \log_2 N \rfloor\). Then \(\binom{N}{r} \le \prod_{k=1}^{L} a_k\), where \(a_1 = P(r)\) and \(a_k = P(\lfloor N^{1/k} \rfloor)\) for \(k \ge 2\).

This matches the product estimate in Erdős's proof.

theorem choose_le_prod_erdos_layers_of_no_large {N r : ℕ} (hN : 0 < N)
    (hrN : r ≤ N) (hsmall : ∀ p : ℕ, p.Prime → p ∣ Nat.choose N r → p ≤ r) :
    Nat.choose N r ≤
      ∏ j ∈ Finset.range (Nat.log 2 N),
        if j = 0 then primorial r else primorial (Nat.nthRoot (j + 1) N)

Uses 1 · Used by 2

Proof usesTruncating the prime factorization of a binomial coefficient

Used byA numerical criterion for a prime divisor of \(\binom{N}{r}\) above \(r\) when \(N \ge 3r\) · Large-prime criterion from the Erdős layer bound

TheoremErdős layer bound with a one-third first layer#✓fully proved

Let \(N \ge 6\) and \(r\) be natural numbers with \(2r \le N\) (hence \(r \le N\)) such that every prime divisor of \(\binom{N}{r}\) is at most \(r\). Write \(P(m)\) for the product of all primes \(p \le m\) and let \(L = \lfloor \log_2 N \rfloor\). Then \(\binom{N}{r} \le \prod_{k=1}^{L} a_k\), where \(a_1 = P(\lfloor N/3 \rfloor)\) and \(a_k = P(\lfloor N^{1/k} \rfloor)\) for \(k \ge 2\).

theorem choose_le_prod_erdos_div_three_layers_of_no_large {N r : ℕ} (hN : 0 < N)
    (hrN : r ≤ N) (h2rN : 2 * r ≤ N) (hN6 : 6 ≤ N)
    (hsmall : ∀ p : ℕ, p.Prime → p ∣ Nat.choose N r → p ≤ r) :
    Nat.choose N r ≤
      ∏ j ∈ Finset.range (Nat.log 2 N),
        if j = 0 then primorial (N / 3) else primorial (Nat.nthRoot (j + 1) N)

Uses 1 · Used by 3

Proof usesTruncating the prime factorization of a binomial coefficient

Used byErdős layer criterion, factorial form · Erdős layer criterion, power-of-four form · A numerical criterion for a prime divisor of \(\binom{N}{r}\) above \(r\) when \(N = 2r + i\)

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.