English
For N with N ≥ 4096, N·exp(−4√(ln N)) is strictly less than rothNumberNat N.
Русский
Для N с N ≥ 4096, N e^{−4√(ln N)} меньше rothNumberNat N.
LaTeX
$$$$ N \\cdot \\exp(-4 \\sqrt{\\log N}) < \\operatorname{rothNumberNat} N \\quad (N \\ge 4096). $$$$
Lean4
theorem le_N (hN : 2 ≤ N) : (2 * dValue N - 1) ^ nValue N ≤ N :=
by
have : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N := Nat.pow_le_pow_left (Nat.sub_le _ _) _
apply this.trans
suffices ((2 * dValue N) ^ nValue N : ℝ) ≤ N from mod_cast this
suffices i : (2 * dValue N : ℝ) ≤ (N : ℝ) ^ (nValue N : ℝ)⁻¹
by
rw [← rpow_natCast]
apply (rpow_le_rpow (mul_nonneg zero_le_two (cast_nonneg _)) i (cast_nonneg _)).trans
rw [← rpow_mul (cast_nonneg _), inv_mul_cancel₀, rpow_one]
rw [cast_ne_zero]
apply (nValue_pos hN).ne'
rw [← le_div_iff₀']
· exact floor_le (div_nonneg (rpow_nonneg (cast_nonneg _) _) zero_le_two)
apply zero_lt_two
