choose_middle_le_pow — Mathlib

English

The middle binomial coefficient is bounded by a power of 4: (2n+1 choose n) ≤ 4^n.

Русский

Серединный биномиальный коэффициент ограничен сверху степенью 4: (2n+1 choose n) ≤ 4^n.

LaTeX

$$$\binom{2n+1}{n} \le 4^n$$$

Lean4

theorem choose_middle_le_pow (n : ℕ) : (2 * n + 1).choose n ≤ 4 ^ n :=
  by
  have t : (2 * n + 1).choose n ≤ ∑ i ∈ range (n + 1), (2 * n + 1).choose i :=
    single_le_sum (fun x _ ↦ by cutsat) (self_mem_range_succ n)
  simpa [sum_range_choose_halfway n] using t

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