English
If N ≥ 4096, then (N)^{nValue(N)^{-1}} / e < dValue(N).
Русский
При N ≥ 4096 выполняется (N)^{1/nValue(N)} / e < dValue(N).
LaTeX
$$$$ \\frac{N^{1/nValue(N)}}{e} < dValue(N) \\quad\\text{for } N \\ge 4096. $$$$
Lean4
theorem dValue_pos (hN₃ : 8 ≤ N) : 0 < dValue N :=
by
have hN₀ : 0 < (N : ℝ) := cast_pos.2 (succ_pos'.trans_le hN₃)
rw [dValue, floor_pos, ← log_le_log_iff zero_lt_one, log_one, log_div _ two_ne_zero, log_rpow hN₀, inv_mul_eq_div,
sub_nonneg, le_div_iff₀]
· have : (nValue N : ℝ) ≤ 2 * √(log N) :=
by
apply (ceil_lt_add_one <| sqrt_nonneg _).le.trans
rw [two_mul, add_le_add_iff_left]
apply le_sqrt_of_sq_le
rw [one_pow, le_log_iff_exp_le hN₀]
exact (exp_one_lt_d9.le.trans <| by norm_num).trans (cast_le.2 hN₃)
apply (mul_le_mul_of_nonneg_left this <| log_nonneg one_le_two).trans _
rw [← mul_assoc, ← le_div_iff₀ (Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 _), div_sqrt]
· apply log_two_mul_two_le_sqrt_log_eight.trans
apply Real.sqrt_le_sqrt
exact log_le_log (by simp) (mod_cast hN₃)
exact hN₃.trans_lt' (by simp)
· exact cast_pos.2 (nValue_pos <| hN₃.trans' <| by simp)
· exact (rpow_pos_of_pos hN₀ _).ne'
· exact div_pos (rpow_pos_of_pos hN₀ _) zero_lt_two
