Ramanujan.epsilon_bound

@[blueprint  "epsilon-bound"  (title := "Bound for εMₐ - εmₐ")  (statement := /-- We have $\epsilon_{M_a} - \epsilon'_{m_a} < \log (e x_a )$. -/)  (proof := /-- This is a direct calculation. An AI verification can be found at https://chatgpt.com/share/69a64f96-b1cc-800e-8f85-850168d23094  -/)  (latexEnv := "lemma")  (discussion := 998)]theorem epsilon_bound :  ∀ x > exₐ, ε (Mₐ exₐ) x - εlower (mₐ xₐ) xₐ x < log x := by  intro x hx  have log_gt_3915 : (3915 : ℝ) < log x := by    simpa [exₐ_eq, log_exp] using log_lt_log exₐ_pos hx  have := Mₐ_exₐ_nonneg  have := Mₐ_exₐ_le_1426  have : (2 * Mₐ exₐ + 132) / log x ≤ (2 * (1426 : ℝ) + 132) / (3915 : ℝ) :=    le_trans (div_le_div_of_nonneg_left (by nlinarith) (by positivity) log_gt_3915.le)      (div_le_div_of_nonneg_right (by nlinarith) (by positivity))  have : (4 * Mₐ exₐ + 288) / (log x) ^ 2 ≤ (4 * (1426 : ℝ) + 288) / (3915 : ℝ) ^ 2 :=    le_trans (div_le_div_of_nonneg_left (by nlinarith) (by positivity) (by grind [pow_le_pow_left₀]))      (div_le_div_of_nonneg_right (by nlinarith) (by positivity))  have : (12 * Mₐ exₐ + 576) / (log x) ^ 3 ≤ (12 * (1426 : ℝ) + 576) / (3915 : ℝ) ^ 3 :=    le_trans (div_le_div_of_nonneg_left (by nlinarith) (by positivity) (by grind [pow_le_pow_left₀]))      (div_le_div_of_nonneg_right (by nlinarith) (by positivity))  have : (48 * Mₐ exₐ) / (log x) ^ 4 ≤ (48 * (1426 : ℝ)) / (3915 : ℝ) ^ 4 :=    le_trans (div_le_div_of_nonneg_left (by nlinarith) (by positivity) (by grind [pow_le_pow_left₀]))      (div_le_div_of_nonneg_right (by nlinarith) (by positivity))  have : (Mₐ exₐ ^ 2) / (log x) ^ 5 ≤ ((1426 : ℝ) ^ 2) / (3915 : ℝ) ^ 5 :=    le_trans (div_le_div_of_nonneg_left (sq_nonneg _) (by positivity) (by grind [pow_le_pow_left₀]))      (div_le_div_of_nonneg_right (by nlinarith) (by positivity))  have : 0 ≤ 364 / log x := by positivity  have : 0 ≤ 381 / (log x) ^ 2 := by positivity  have : 0 ≤ 238 / (log x) ^ 3 := by positivity  have : 0 ≤ 97 / (log x) ^ 4 := by positivity  have : 0 ≤ 30 / (log x) ^ 5 := by positivity  have : 0 ≤ 8 / (log x) ^ 6 := by positivity  by_cases hm : 0 ≤ mₐ xₐ  · rw [εlower, if_pos hm]    unfold ε ε'    linarith  · rw [εlower, if_neg hm]    have := mₐ_xₐ_ge_neg1194    have halpha_tight : (1 + 1 / log xₐ) ^ 6 ≤ (10016 : ℝ) / 10000 := by      rw [log_xₐ_val]; norm_num    unfold ε εneg    nlinarith [mul_le_mul_of_nonpos_right halpha_tight (by linarith : mₐ xₐ ≤ 0)]