FKS2.Epi_le_evalLhsE_wide

theorem Epi_le_evalLhsE_wide (x : ℝ) (h5 : Real.exp 5 ≤ x) (h40 : x ≤ Real.exp 40) :    Eπ x ≤ Expr.eval (fun _ => Real.sqrt (Real.log x)) FloorButhe.lhsE := by  have he5 : (2:ℝ) ≤ Real.exp 5 := by    have := Real.add_one_le_exp (5:ℝ); linarith  have hx2 : (2:ℝ) ≤ x := le_trans he5 h5  have hxpos : (0:ℝ) < x := by linarith  have hLge5 : (5:ℝ) ≤ Real.log x := by    rw [← Real.log_exp 5]; exact Real.log_le_log (Real.exp_pos _) h5  have hLpos : (0:ℝ) < Real.log x := by linarith  have hLnn : (0:ℝ) ≤ Real.log x := le_of_lt hLpos  have hx19 : x ≤ 10 ^ 19 := by    have h2 : Real.exp 40 ≤ (2.72:ℝ) ^ 40 := by      have he : Real.exp 40 = Real.exp 1 ^ 40 := by rw [← Real.exp_nat_mul]; norm_num      rw [he]; gcongr      linarith [Real.exp_one_lt_d9]    have h3 : (2.72:ℝ) ^ 40 ≤ 10 ^ 19 := by norm_num    linarith [h40]  have h2e := Buthe.theorem_2e hx2 hx19  have h2f := Buthe.theorem_2f hx2 hx19  have hsub := li.sub_Li x hx2  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