Scaling bounds for binomial coefficients

Scaling the ground set by q scales the number of d-subsets by at least q ^ d (Nat.pow_mul_choose_le_choose_mul). Consequently a fixed d-subset of the ground set lies in at most a q ^ (-d) fraction of the k-subsets when the ground set has at least q k elements (Nat.pow_mul_choose_sub_le_choose). Lowering ℓ by s scales the number of ℓ-subsets of an m-set by at most (ℓ / (m - ℓ + 1)) ^ s (Nat.choose_sub_mul_pow_le), so by at most q ^ (-s) when (q + 1) ℓ ≤ m (Nat.pow_mul_choose_sub_le_choose_of_mul_le). Conversely, descending factorials and binomial coefficients grow at least as fast as powers on larger ground sets (Nat.descFactorial_mul_pow_le, Nat.choose_mul_pow_le), which gives the block-avoidance estimate 2 ^ r * C(b * m - m, b * r) ≤ C(b * m, b * r) (Nat.two_pow_mul_choose_sub_le).

Main results

• Nat.pow_mul_descFactorial_le, Nat.pow_mul_choose_le_choose_mul, Nat.pow_mul_choose_sub_le_choose: scaling the ground set scales descending factorials and binomial coefficients.
• Nat.choose_sub_mul_pow_le, Nat.pow_mul_choose_sub_le_choose_of_mul_le: lowering the subset size scales the binomial coefficient.
• Nat.descFactorial_mul_pow_le, Nat.choose_mul_pow_le, Nat.choose_mul_sub_mul_pow_le, Nat.two_mul_pred_pow_le, Nat.two_pow_mul_choose_sub_le: power comparisons and the block-avoidance binomial estimate.

theorem Nat.pow_mul_descFactorial_le {q : ℕ} (hq : 1 ≤ q) {k d : ℕ} (hd : d ≤ k) : q ^ d * k.descFactorial d ≤ (q * k).descFactorial d

Scaling the ground set by q ≥ 1 scales a descending factorial by at least q ^ d.

theorem Nat.pow_mul_choose_le_choose_mul {q : ℕ} (hq : 1 ≤ q) {k d : ℕ} (hd : d ≤ k) : q ^ d * k.choose d ≤ (q * k).choose d

Scaling the ground set by q ≥ 1 scales the number of d-subsets by at least q ^ d.

theorem Nat.pow_mul_choose_sub_le_choose {q n k d : ℕ} (hq : 1 ≤ q) (hd : d ≤ k) (hn : q * k ≤ n) : q ^ d * (n - d).choose (k - d) ≤ n.choose k

A d-subset of an n-set lies in at most a q ^ (-d) fraction of its k-subsets when q k ≤ n.

theorem Nat.choose_sub_mul_pow_le {m ℓ s : ℕ} (hs : s ≤ ℓ) (hℓ : ℓ ≤ m) : m.choose (ℓ - s) * (m - ℓ + 1) ^ s ≤ m.choose ℓ * ℓ ^ s

Lowering ℓ by s scales the number of ℓ-subsets of an m-set by at most (ℓ / (m - ℓ + 1)) ^ s.

theorem Nat.pow_mul_choose_sub_le_choose_of_mul_le {m ℓ s q : ℕ} (hs : s ≤ ℓ) (hℓ : (q + 1) * ℓ ≤ m) : q ^ s * m.choose (ℓ - s) ≤ m.choose ℓ

If ℓ and q ℓ together fit into m, lowering ℓ by s ≤ ℓ divides the number of ℓ-subsets of an m-set by at least q ^ s.

theorem Nat.descFactorial_mul_pow_le {s n : ℕ} (h : s ≤ n) (k : ℕ) : s.descFactorial k * n ^ k ≤ s ^ k * n.descFactorial k

Descending factorials compare like powers: s^{(k)} / n^{(k)} ≤ (s / n)^k for s ≤ n.

theorem Nat.choose_mul_pow_le {a s : ℕ} (has : a ≤ s) (k : ℕ) : a.choose k * s ^ k ≤ s.choose k * a ^ k

For a ≤ s, C(a, k) * s ^ k ≤ C(s, k) * a ^ k.

theorem Nat.choose_mul_sub_mul_pow_le (b m k : ℕ) : (b * m - m).choose k * b ^ k ≤ (b * m).choose k * (b - 1) ^ k

C(b * m - m, k) * b ^ k ≤ C(b * m, k) * (b - 1) ^ k.

theorem Nat.two_mul_pred_pow_le {b : ℕ} (hb : 1 ≤ b) : 2 * (b - 1) ^ b ≤ b ^ b

For 1 ≤ b, 2 * (b - 1) ^ b ≤ b ^ b.

theorem Nat.two_pow_mul_choose_sub_le {b m : ℕ} (hb : 1 ≤ b) (r : ℕ) : 2 ^ r * (b * m - m).choose (b * r) ≤ (b * m).choose (b * r)

For 1 ≤ b, 2 ^ r * C(b * m - m, b * r) ≤ C(b * m, b * r).