Inequalities for binomial coefficients #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

theorem nat.choose_le_pow {α : Type u_1} [linear_ordered_semifield α] (r n : ℕ) :

↑(n.choose r) ≤ ↑n ^ r / ↑(r.factorial)

source

theorem nat.pow_le_choose {α : Type u_1} [linear_ordered_semifield α] (r n : ℕ) :

↑(n + 1 - r) ^ r / ↑(r.factorial) ≤ ↑(n.choose r)