four_pow_le_two_mul_add_one_mul_central_binom

English

A chain of inequalities shows 4^n ≤ (2n+1)·(2n choose n), providing a lower bound via central binomial growth.

Русский

Цепь неравенств демонстрирует 4^n ≤ (2n+1)·(2n choose n), задавая нижнюю границу через центральный мультиномиал.

LaTeX

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

Lean4

theorem four_pow_le_two_mul_add_one_mul_central_binom (n : ℕ) : 4 ^ n ≤ (2 * n + 1) * (2 * n).choose n :=
  calc
    4 ^ n = (1 + 1) ^ (2 * n) := by simp [pow_mul]
    _ = ∑ m ∈ range (2 * n + 1), (2 * n).choose m := by simp [-Nat.reduceAdd, add_pow]
    _ ≤ ∑ _ ∈ range (2 * n + 1), (2 * n).choose (2 * n / 2) := by gcongr; apply choose_le_middle
    _ = (2 * n + 1) * choose (2 * n) n := by simp

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