Documentation

Mathlib.Data.Nat.Choose.Bounds

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 #

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_lt_descFactorial {n k : } (hk : 2 k) (hkn : k n) :
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.pow_le_choose {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (r n : ) :
↑(n + 1 - r) ^ r / r.factorial (n.choose r)
@[irreducible]
theorem Nat.choose_succ_le_two_pow (n k : ) :
(n + 1).choose k 2 ^ n
theorem Nat.choose_le_two_pow (n k : ) (p : 0 < n) :
n.choose k < 2 ^ n