FKS2.Table4Ext.Epi_le_evalLhsE_low

theorem Epi_le_evalLhsE_low (x : ℝ) (h2 : (2 : ℝ) ≤ x) (h10 : x ≤ Real.exp 10) :    Eπ x ≤ Expr.eval (fun _ => Real.sqrt (Real.log x)) FloorButhe.lhsE := by  have hxpos : (0:ℝ) < x := by linarith  have hLpos : (0:ℝ) < Real.log x := Real.log_pos (by linarith)  have hLnn : (0:ℝ) ≤ Real.log x := le_of_lt hLpos  have hx19 : x ≤ 10 ^ 19 := by    have h2' : Real.exp 10 < (3:ℝ) ^ 10 := by      calc Real.exp 10 = Real.exp 1 ^ 10 := by rw [← Real.exp_nat_mul]; norm_num        _ < 3 ^ 10 := by            have h1 := Real.exp_one_lt_d9            have hlt : Real.exp 1 < 3 := by linarith            gcongr    have h3 : (3:ℝ) ^ 10 ≤ 10 ^ 19 := by norm_num    linarith [h10]  have h2e := Buthe.theorem_2e h2 hx19  have h2f := Buthe.theorem_2f h2 hx19  have hsub := li.sub_Li x h2  have hli2 := li.two_approx  have hli2_le : li 2 ≤ 1.0452 := hli2.2  have hpiLi : pi x - Li x = li 2 - (li x - pi x) := by linarith [hsub]  have habs : |pi x - Li x| ≤ (li x - pi x) + li 2 := by    rw [hpiLi, abs_le]    constructor <;> linarith [h2f, hli2.1]  have hEpi_eq : Eπ x = |pi x - Li x| * (Real.log x / x) := by    unfold Eπ    rw [div_div_eq_mul_div, mul_div_assoc]  rw [hEpi_eq]  set B := Real.sqrt x / Real.log x * (1.95 + 3.9 / Real.log x + 19.5 / (Real.log x) ^ 2) with hB_def  have hfactor_nn : (0:ℝ) ≤ Real.log x / x := by positivity  have hstep1 : |pi x - Li x| * (Real.log x / x) ≤ (B + 1.0452) * (Real.log x / x) := by    apply mul_le_mul_of_nonneg_right _ hfactor_nn    calc |pi x - Li x| ≤ (li x - pi x) + li 2 := habs      _ ≤ B + 1.0452 := by          apply add_le_add          · rw [hB_def]; exact h2e          · exact hli2_le  refine le_trans hstep1 (le_of_eq ?_)  have hxne : x ≠ 0 := ne_of_gt hxpos  have hLne : Real.log x ≠ 0 := ne_of_gt hLpos  have hxinv : x⁻¹ = Real.exp (-(Real.log x)) := by    rw [Real.exp_neg, Real.exp_log hxpos]  have hsqrtx : Real.sqrt x = Real.exp (Real.log x / 2) := by    rw [← Real.exp_log (Real.sqrt_pos.mpr hxpos), Real.log_sqrt (le_of_lt hxpos)]  set s := Real.sqrt (Real.log x) with hs_def  have hss : s * s = Real.log x := by rw [hs_def]; exact Real.mul_self_sqrt hLnn  rw [FloorButhe.eval_lhsE, hss]  set L := Real.log x with hL_def  have hLx : L / x = L * Real.exp (-L) := by    rw [div_eq_mul_inv, hxinv]  have hsqrtxE2 : Real.sqrt x * Real.exp (-L) = Real.exp (-L / 2) := by    rw [hsqrtx, ← Real.exp_add]; congr 1; ring  rw [hB_def, hLx]  rw [show (Real.sqrt x / L * (1.95 + 3.9 / L + 19.5 / L ^ 2) + 1.0452) * (L * Real.exp (-L))      = (Real.sqrt x * Real.exp (-L)) * (1.95 + 3.9 / L + 19.5 / L ^ 2)        + 1.0452 * (L * Real.exp (-L)) by        field_simp]  rw [hsqrtxE2]  ring