English
For n ≥ 4, 4^n < n · centralBinom(n).
Русский
При n ≥ 4: 4^n < n · centralBinom(n).
LaTeX
$$$$ 4^{n} < n \\cdot \\binom{2n}{n} \\quad (n \\ge 4). $$$$
Lean4
/-- An exponential lower bound on the central binomial coefficient.
This bound is of interest because it appears in
[Tochiori's refinement of Erdős's proof of Bertrand's postulate](tochiori_bertrand).
-/
theorem four_pow_lt_mul_centralBinom (n : ℕ) (n_big : 4 ≤ n) : 4 ^ n < n * centralBinom n :=
by
induction n using Nat.strong_induction_on with
| _ n IH
rcases lt_trichotomy n 4 with (hn | rfl | hn)
· clear IH; exact False.elim ((not_lt.2 n_big) hn)
· norm_num [centralBinom, choose]
obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := Nat.exists_eq_succ_of_ne_zero (Nat.ne_zero_of_lt hn)
calc
4 ^ (n + 1)
_ = 4 * 4 ^ n := by rw [pow_succ']
_ < 4 * (n * centralBinom n) := by gcongr; exact IH n n.lt_succ_self (Nat.le_of_lt_succ hn)
_ ≤ 2 * (2 * n + 1) * centralBinom n := by rw [← mul_assoc]; linarith
_ = (n + 1) * centralBinom (n + 1) := (succ_mul_centralBinom_succ n).symm
