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