Inequalities for binomial coefficients

This file proves exponential bounds on binomial coefficients. We might want to add here the bounds n^r/r^r ≤ n.choose r ≤ e^r n^r/r^r in the future.

Main declarations

• Nat.choose_le_pow_div: n.choose r ≤ n^r / r!
• Nat.pow_le_choose: (n + 1 - r)^r / r! ≤ n.choose r. Beware of the fishy ℕ-subtraction.

theorem Nat.choose_le_pow_div {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (r n : ℕ) : ↑(n.choose r) ≤ ↑n ^ r / ↑r.factorial

theorem Nat.choose_lt_pow_div {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {n k : ℕ} (hn : n ≠ 0) (hk : 2 ≤ k) : ↑(n.choose k) < ↑n ^ k / ↑k.factorial

theorem Nat.choose_le_descFactorial (n k : ℕ) : n.choose k ≤ n.descFactorial k

theorem Nat.choose_lt_descFactorial {n k : ℕ} (hk : 2 ≤ k) (hkn : k ≤ n) : n.choose k < n.descFactorial k

theorem Nat.choose_le_pow (n k : ℕ) : n.choose k ≤ n ^ k

theorem Nat.choose_lt_pow {n k : ℕ} (hn : n ≠ 0) (hk : 2 ≤ k) : n.choose k < n ^ k

theorem Nat.choose_add_le_add_one_pow (n k : ℕ) : (n + k).choose k ≤ (n + 1) ^ k

theorem Nat.choose_le_sub_pow (n k : ℕ) : n.choose k ≤ (n + 1 - k) ^ k

theorem Nat.pow_le_choose {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (r n : ℕ) : ↑(n + 1 - r) ^ r / ↑r.factorial ≤ ↑(n.choose r)

theorem Nat.choose_succ_le_two_pow (n k : ℕ) : (n + 1).choose k ≤ 2 ^ n

theorem Nat.choose_lt_two_pow (n k : ℕ) (p : 0 < n) : n.choose k < 2 ^ n

theorem Nat.choose_le_two_pow (n k : ℕ) : n.choose k ≤ 2 ^ n