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 : ℕ)
:
theorem
Nat.choose_lt_pow_div
{α : Type u_1}
[Semifield α]
[LinearOrder α]
[IsStrictOrderedRing α]
{n k : ℕ}
(hn : n ≠ 0)
(hk : 2 ≤ k)
:
theorem
Nat.pow_le_choose
{α : Type u_1}
[Semifield α]
[LinearOrder α]
[IsStrictOrderedRing α]
(r n : ℕ)
: