English
For all n>0, 4^n ≤ 2·n·centralBinom(n).
Русский
Для всех n>0: 4^n ≤ 2·n·centralBinom(n).
LaTeX
$$$$ 4^{n} \\le 2\\,n\\, \\binom{2n}{n}. $$$$
Lean4
/-- An exponential lower bound on the central binomial coefficient.
This bound is weaker than `Nat.four_pow_lt_mul_centralBinom`, but it is of historical interest
because it appears in Erdős's proof of Bertrand's postulate.
-/
theorem four_pow_le_two_mul_self_mul_centralBinom : ∀ (n : ℕ) (_ : 0 < n), 4 ^ n ≤ 2 * n * centralBinom n
| 0, pr => (Nat.not_lt_zero _ pr).elim
| 1, _ => by simp [centralBinom, choose]
| 2, _ => by simp [centralBinom, choose]
| 3, _ => by simp [centralBinom, choose]
| n + 4, _ =>
calc
4 ^ (n + 4) ≤ (n + 4) * centralBinom (n + 4) := (four_pow_lt_mul_centralBinom _ le_add_self).le
_ ≤ 2 * (n + 4) * centralBinom (n + 4) := by rw [mul_assoc]; refine Nat.le_mul_of_pos_left _ zero_lt_two
