English
For any N with 4096 ≤ N, log(2/(1−2/exp 1)) * (69/50) ≤ √(log N).
Русский
Для любого N с 4096 ≤ N выполнено неравенство: log(2/(1−2/e)) · (69/50) ≤ √(log N).
LaTeX
$$$ \\log(2/(1 - 2/\\exp 1)) \\cdot \\frac{69}{50} \\le \\sqrt{\\log N} \\quad (4096 \\le N) $$$
Lean4
theorem le_sqrt_log (hN : 4096 ≤ N) : log (2 / (1 - 2 / exp 1)) * (69 / 50) ≤ √(log ↑N) := by
calc
_ ≤ log (2 ^ 3) * (69 / 50) := by
gcongr
· field_simp
simp (disch := positivity) [show 2 < Real.exp 1 from lt_trans (by norm_num1) exp_one_gt_d9]
· norm_num1
exact two_div_one_sub_two_div_e_le_eight
_ ≤ √(log (2 ^ 12)) := by
simp only [Real.log_pow, Nat.cast_ofNat]
apply le_sqrt_of_sq_le
nlinarith [log_two_lt_d9, log_two_gt_d9]
_ ≤ √(log ↑N) := by
gcongr
exact mod_cast hN
