English
For all N ≥ 0, (N)·exp(−4√(ln N)) ≤ rothNumberNat N.
Русский
Для всех N ≥ 0 верно (N) e^{−4√(ln N)} ≤ rothNumberNat N.
LaTeX
$$$$ N \\cdot \\exp(-4 \\sqrt{\\log N}) \\le rothNumberNat N. $$$$
Lean4
theorem bound (hN : 4096 ≤ N) : (N : ℝ) ^ (nValue N : ℝ)⁻¹ / exp 1 < dValue N :=
by
apply div_lt_floor _
rw [← log_le_log_iff, log_rpow, mul_comm, ← div_eq_mul_inv, nValue]
· grw [ceil_lt_mul]
· rw [mul_comm, ← div_div, div_sqrt, le_div_iff₀]
· norm_num [le_sqrt_log hN]
· norm_num1
· rw [cast_pos, lt_ceil, cast_zero, Real.sqrt_pos]
refine log_pos ?_
rw [one_lt_cast]
exact hN.trans_lt' (by norm_num1)
apply le_sqrt_of_sq_le
have : (12 : ℕ) * log 2 ≤ log N := by
rw [← log_rpow zero_lt_two, rpow_natCast]
exact log_le_log (by positivity) (mod_cast hN)
refine le_trans ?_ this
rw [← div_le_iff₀']
· exact log_two_gt_d9.le.trans' (by norm_num1)
· norm_num1
· rw [cast_pos]
exact hN.trans_lt' (by norm_num1)
· refine div_pos zero_lt_two ?_
rw [sub_pos, div_lt_one (exp_pos _)]
exact lt_of_le_of_lt (by norm_num1) exp_one_gt_d9
positivity
