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: 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 {α : Type u_1} [LinearOrderedSemifield α] (r : ℕ) (n : ℕ) : ↑(n.choose r) ≤ ↑n ^ r / ↑r.factorial

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