FKS2.FloorButhe4.rhsE4_le_rowcurve

theorem rhsE4_le_rowcurve (x : ℝ) (hL : (5 : ℝ) ≤ Real.log x) :    Expr.eval (fun _ => Real.sqrt (Real.log x)) rhsE4      ≤ admissible_bound 1.76 1 1.5 5.5666305 x := by  have hLnn : (0:ℝ) ≤ Real.log x := le_trans (by norm_num) hL  rw [eval_rhsE4, admissible_one_eq 1.76 1.5 5.5666305 x hLnn (by norm_num)]  set s := Real.sqrt (Real.log x) with hs_def  have hs_nn : (0:ℝ) ≤ s := Real.sqrt_nonneg _  have hss : s * s = s ^ 2 := by ring  have hsqrtR_lb := sqrtR5_lb  have hsqrtR_pos := sqrtR5_pos  have hcoeff : (316/1000:ℝ) ≤ 1.76 / (5.5666305:ℝ) := by    rw [le_div_iff₀ (by norm_num)]; norm_num  have hCR : (1.5:ℝ) / Real.sqrt 5.5666305 ≤ 63577/100000 := by    rw [div_le_iff₀ hsqrtR_pos]; nlinarith [hsqrtR_lb]  have hexpRHS : Real.exp (-(63577/100000:ℝ) * s) ≤ Real.exp (-(1.5 / Real.sqrt 5.5666305) * s) := by    apply Real.exp_le_exp.mpr    have hCRs : (1.5 / Real.sqrt 5.5666305) * s ≤ (63577/100000) * s :=      mul_le_mul_of_nonneg_right hCR hs_nn    simp only [neg_mul]; linarith [hCRs]  have hs2 : (0:ℝ) ≤ s ^ 2 := by positivity  rw [hss]  calc (316/1000:ℝ) * s ^ 2 * Real.exp (-(63577/100000) * s)      = ((316/1000:ℝ) * Real.exp (-(63577/100000) * s)) * s ^ 2 := by ring    _ ≤ ((1.76 / 5.5666305) * Real.exp (-(1.5 / Real.sqrt 5.5666305) * s)) * s ^ 2 :=        mul_le_mul_of_nonneg_right          (mul_le_mul hcoeff hexpRHS (Real.exp_nonneg _) (by positivity)) hs2    _ = 1.76 / 5.5666305 * s ^ 2 * Real.exp (-(1.5 / Real.sqrt 5.5666305) * s) := by ring