mathlib documentation


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 #

theorem nat.choose_le_pow {α : Type u_1} [linear_ordered_semifield α] (r n : ) :
theorem nat.pow_le_choose {α : Type u_1} [linear_ordered_semifield α] (r n : ) :
(n + 1 - r) ^ r / (r.factorial) (n.choose r)