FKS2.floor_buthe_quarter_wide

theorem floor_buthe_quarter_wide (rhsE2 : Expr) (A C : ℝ) (xlo xhi : ℝ) (slabLo : ℚ) (n : ℕ)    (hApos : 0 < A)    (hxlo5 : (5:ℝ) ≤ xlo) (hxhi40 : xhi ≤ 40)    (hslo : (slabLo:ℝ) ≤ Real.sqrt xlo)    (hshi : Real.sqrt xhi < (slabLo:ℝ) + (n:ℝ) * 0.05)    (hchk : checkExprLeOnSlabsDyadic (Expr.mul FloorButhe.lhsE FloorButhe.lhsE) rhsE2        (slabsFrom slabLo n) (-50) 8 = true)    (hcurve2 : ∀ x, xlo ≤ Real.log x →        Expr.eval (fun _ => Real.sqrt (Real.log x)) rhsE2          ≤ (admissible_bound A 0.25 C 5.5666305 x) ^ 2) :    ∀ x ∈ Set.Icc (Real.exp xlo) (Real.exp xhi),      Eπ x ≤ admissible_bound A 0.25 C 5.5666305 x := by  intro x hx  obtain ⟨hlo, hhi⟩ := hx  have h5 : Real.exp 5 ≤ x := le_trans (Real.exp_le_exp.mpr hxlo5) hlo  have h40 : x ≤ Real.exp 40 := le_trans hhi (Real.exp_le_exp.mpr hxhi40)  have hxpos : (0 : ℝ) < x := lt_of_lt_of_le (Real.exp_pos _) h5  have hLgexlo : xlo ≤ Real.log x := by    rw [← Real.log_exp xlo]; exact Real.log_le_log (Real.exp_pos _) hlo  have hLlexhi : Real.log x ≤ xhi := by    rw [← Real.log_exp xhi]; exact Real.log_le_log hxpos hhi  have hLpos : (0:ℝ) < Real.log x := lt_of_lt_of_le (by linarith) hLgexlo  have hcov_lo : (slabLo:ℝ) ≤ Real.sqrt (Real.log x) :=    le_trans hslo (Real.sqrt_le_sqrt hLgexlo)  have hcov_hi : Real.sqrt (Real.log x) < (slabLo:ℝ) + (n:ℝ) * 0.05 :=    lt_of_le_of_lt (Real.sqrt_le_sqrt hLlexhi) hshi  obtain ⟨I, hI, hmem⟩ := coverFrom slabLo n _ hcov_lo hcov_hi  have hslab2 := verify_expr_le_on_slabs_dyadic (Expr.mul FloorButhe.lhsE FloorButhe.lhsE) rhsE2    (slabsFrom slabLo n) (-50) 8 (by norm_num) hchk I hI _ hmem  rw [Expr.eval_mul] at hslab2  set Lh := Expr.eval (fun _ => Real.sqrt (Real.log x)) FloorButhe.lhsE with hLh_def  have hLh_nn : (0:ℝ) ≤ Lh := by    rw [hLh_def, FloorButhe.eval_lhsE]; positivity  have hadm_nn : (0:ℝ) ≤ admissible_bound A 0.25 C 5.5666305 x := by    rw [admissible_quarter_eq A C 5.5666305 x hLpos.le (by norm_num)]; positivity  have hsq : Lh ^ 2 ≤ (admissible_bound A 0.25 C 5.5666305 x) ^ 2 := by    calc Lh ^ 2 = Lh * Lh := sq Lh      _ ≤ Expr.eval (fun _ => Real.sqrt (Real.log x)) rhsE2 := hslab2      _ ≤ (admissible_bound A 0.25 C 5.5666305 x) ^ 2 := hcurve2 x hLgexlo  have hLh_le : Lh ≤ admissible_bound A 0.25 C 5.5666305 x := by    have := Real.sqrt_le_sqrt hsq    rwa [Real.sqrt_sq hLh_nn, Real.sqrt_sq hadm_nn] at this  exact le_trans (Epi_le_evalLhsE_wide x h5 h40) hLh_le