choose_le_middle — Mathlib

English

The binomial coefficient is maximized at the middle, i.e., C(n,r) ≤ C(n,n/2) for all r.

Русский

Биномиальный коэффициент достигает максимума в середине: C(n,r) ≤ C(n, ⌊n/2⌋) для всех r.

LaTeX

$$$$ \binom{n}{r} \le \binom{n}{\left\lfloor \frac{n}{2} \right\rfloor} $$$$

Lean4

/-- `choose n r` is maximised when `r` is `n/2`. -/
theorem choose_le_middle (r n : ℕ) : choose n r ≤ choose n (n / 2) :=
  by
  rcases le_or_gt r n with b | b
  · rcases le_or_gt r (n / 2) with a | h
    · apply choose_le_middle_of_le_half_left a
    · rw [← choose_symm b]
      apply choose_le_middle_of_le_half_left
      cutsat
  · rw [choose_eq_zero_of_lt b]
    apply zero_le

Похожие утверждения