English
A natural-number version of Bertrand’s bound: for n ≥ 512, n(2n)^√(2n) 4^{2n/3} ≤ 4^n.
Русский
Натуральная версия границы Бернанди: при n ≥ 512 выполняется неравенство.
LaTeX
$$bertrand_main_inequality(n_large) : n * (2 * n) ^ sqrt(2 * n) * 4 ^ (2 * n / 3) ≤ 4 ^ n$$
Lean4
/-- The inequality which contradicts Bertrand's postulate, for large enough `n`.
-/
theorem bertrand_main_inequality {n : ℕ} (n_large : 512 ≤ n) : n * (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3) ≤ 4 ^ n :=
by
rw [← @cast_le ℝ]
simp only [cast_mul, cast_pow, ← Real.rpow_natCast, cast_ofNat]
refine _root_.trans ?_ (Bertrand.real_main_inequality (by exact_mod_cast n_large))
gcongr
· have n2_pos : 0 < 2 * n := by positivity
exact mod_cast n2_pos
· exact_mod_cast Real.nat_sqrt_le_real_sqrt
· norm_num1
· exact cast_div_le.trans (by norm_cast)
