English
e^4 < 64.
Русский
e^4 < 64.
LaTeX
$$$$ e^4 < 64. $$$$
Lean4
theorem roth_lower_bound_explicit (hN : 4096 ≤ N) : (N : ℝ) * exp (-4 * √(log N)) < rothNumberNat N :=
by
let n := nValue N
have hn : 0 < (n : ℝ) := cast_pos.2 (nValue_pos <| hN.trans' <| by norm_num1)
have hd : 0 < dValue N := dValue_pos (hN.trans' <| by norm_num1)
have hN₀ : 0 < (N : ℝ) := cast_pos.2 (hN.trans' <| by norm_num1)
have hn₂ : 2 < n := three_le_nValue <| hN.trans' <| by norm_num1
have : (2 * dValue N - 1) ^ n ≤ N := le_N (hN.trans' <| by norm_num1)
calc
_ ≤ (N ^ (nValue N : ℝ)⁻¹ / rexp 1 : ℝ) ^ (n - 2) / n := ?_
_ < _ := by gcongr; exacts [(tsub_pos_of_lt hn₂).ne', bound hN]
_ ≤ rothNumberNat ((2 * dValue N - 1) ^ n) := (bound_aux hd.ne' hn₂.le)
_ ≤ rothNumberNat N := mod_cast rothNumberNat.mono this
rw [← rpow_natCast, div_rpow (rpow_nonneg hN₀.le _) (exp_pos _).le, ← rpow_mul hN₀.le, inv_mul_eq_div,
cast_sub hn₂.le, cast_two, same_sub_div hn.ne', exp_one_rpow, div_div, rpow_sub hN₀, rpow_one, div_div,
div_eq_mul_inv]
gcongr _ * ?_
rw [mul_inv, mul_inv, ← exp_neg, ← rpow_neg (cast_nonneg _), neg_sub, ← div_eq_mul_inv]
have : exp (-4 * √(log N)) = exp (-2 * √(log N)) * exp (-2 * √(log N)) :=
by
rw [← exp_add, ← add_mul]
norm_num
rw [this]
gcongr
· rw [← le_log_iff_exp_le (rpow_pos_of_pos hN₀ _), log_rpow hN₀, ← le_div_iff₀, mul_div_assoc, div_sqrt, neg_mul,
neg_le_neg_iff, div_mul_eq_mul_div, div_le_iff₀ hn]
· gcongr
apply le_ceil
refine Real.sqrt_pos.2 (log_pos ?_)
rw [one_lt_cast]
exact hN.trans_lt' (by norm_num1)
· refine (exp_neg_two_mul_le <| Real.sqrt_pos.2 <| log_pos ?_).le
rw [one_lt_cast]
exact hN.trans_lt' (by norm_num1)
