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 {α : 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)