doc-next-gen

Mathlib.Data.Nat.Choose.Bounds

Module docstring

{"# 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. "}
Nat.choose_le_pow_div theorem
(r n : ℕ) : (n.choose r : α) ≤ (n ^ r : α) / r !
Full source 
theorem choose_le_pow_div (r n : ℕ) : (n.choose r : α) ≤ (n ^ r : α) / r ! := by
  rw [le_div_iff₀']
  · norm_cast
    rw [← Nat.descFactorial_eq_factorial_mul_choose]
    exact n.descFactorial_le_pow r
  exact mod_cast r.factorial_pos
Binomial Coefficient Bound: $\binom{n}{r} \leq \frac{n^r}{r!}$
Informal description
For any natural numbers $r$ and $n$, and for any division monoid $\alpha$, the binomial coefficient $\binom{n}{r}$ (interpreted in $\alpha$) satisfies the inequality: \[ \binom{n}{r} \leq \frac{n^r}{r!} \] where $n^r$ denotes $n$ raised to the power $r$ and $r!$ is the factorial of $r$.
Nat.choose_le_descFactorial theorem
(n k : ℕ) : n.choose k ≤ n.descFactorial k
Full source 
lemma choose_le_descFactorial (n k : ℕ) : n.choose k ≤ n.descFactorial k := by
  rw [choose_eq_descFactorial_div_factorial]
  exact Nat.div_le_self _ _
Binomial Coefficient Bounded by Descending Factorial: $\binom{n}{k} \leq n^{\underline{k}}$
Informal description
For any natural numbers $n$ and $k$, the binomial coefficient $\binom{n}{k}$ is bounded above by the descending factorial $n^{\underline{k}}$, i.e., \[ \binom{n}{k} \leq n^{\underline{k}} \] where $n^{\underline{k}} = n \cdot (n-1) \cdot \ldots \cdot (n-k+1)$.
Nat.choose_le_pow theorem
(n k : ℕ) : n.choose k ≤ n ^ k
Full source 
/-- This lemma was changed on 2024/08/29, the old statement is available
in `Nat.choose_le_pow_div`. -/
lemma choose_le_pow (n k : ℕ) : n.choose k ≤ n ^ k :=
  (choose_le_descFactorial n k).trans (descFactorial_le_pow n k)
Binomial Coefficient Bound: $\binom{n}{k} \leq n^k$
Informal description
For any natural numbers $n$ and $k$, the binomial coefficient $\binom{n}{k}$ is bounded above by $n^k$, i.e., \[ \binom{n}{k} \leq n^k. \]
Nat.pow_le_choose theorem
(r n : ℕ) : ((n + 1 - r : ℕ) ^ r : α) / r ! ≤ n.choose r
Full source 
theorem pow_le_choose (r n : ℕ) : ((n + 1 - r : ℕ) ^ r : α) / r ! ≤ n.choose r := by
  rw [div_le_iff₀']
  · norm_cast
    rw [← Nat.descFactorial_eq_factorial_mul_choose]
    exact n.pow_sub_le_descFactorial r
  exact mod_cast r.factorial_pos
Lower bound for binomial coefficients: $\frac{(n+1-r)^r}{r!} \leq \binom{n}{r}$
Informal description
For any natural numbers $n$ and $r$, and for any type $\alpha$ with appropriate algebraic structure, the following inequality holds: $$\frac{(n + 1 - r)^r}{r!} \leq \binom{n}{r}$$ where $\binom{n}{r}$ is the binomial coefficient.
Nat.choose_succ_le_two_pow theorem
(n k : ℕ) : (n + 1).choose k ≤ 2 ^ n
Full source 
theorem choose_succ_le_two_pow (n k : ℕ) : (n + 1).choose k ≤ 2 ^ n := by
  by_cases lt : n + 1 < k
  · simp [choose_eq_zero_of_lt lt]
  · cases n with
    | zero => cases k <;> simp_all
    | succ n =>
      rcases k with - | k
      · rw [choose_zero_right]
        exact Nat.one_le_two_pow
      · rw [choose_succ_succ', two_pow_succ]
        exact Nat.add_le_add (choose_succ_le_two_pow n k) (choose_succ_le_two_pow n (k + 1))
Binomial Coefficient Bound: $\binom{n+1}{k} \leq 2^n$
Informal description
For any natural numbers $n$ and $k$, the binomial coefficient $\binom{n+1}{k}$ is bounded above by $2^n$.