FKS2.FloorButhe3.rhsE3_le_rowcurve

theorem rhsE3_le_rowcurve (x : ℝ) (hL : (6 : ℝ) ≤ Real.log x) :    Expr.eval (fun _ => Real.sqrt (Real.log x)) rhsE3      ≤ admissible_bound 1.41 0.5 1.5 5.5666305 x := by  have hLnn : (0:ℝ) ≤ Real.log x := le_trans (by norm_num) hL  rw [eval_rhsE3, admissible_half_eq 1.41 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 hsqrtR_lb := sqrtR5_lb  have hsqrtR_ub := sqrtR5_ub  have hsqrtR_pos := sqrtR5_pos  have hcoeff : (5976/10000:ℝ) ≤ 1.41 / Real.sqrt 5.5666305 := by    rw [le_div_iff₀ hsqrtR_pos]; nlinarith [hsqrtR_ub]  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 : (1.5 / Real.sqrt 5.5666305) * s ≤ (63577/100000) * s := mul_le_mul_of_nonneg_right hCR hs_nn    simp only [neg_mul]; linarith  calc (5976/10000:ℝ) * s * Real.exp (-(63577/100000) * s)      = ((5976/10000:ℝ) * Real.exp (-(63577/100000) * s)) * s := by ring    _ ≤ ((1.41 / Real.sqrt 5.5666305) * Real.exp (-(1.5 / Real.sqrt 5.5666305) * s)) * s :=        mul_le_mul_of_nonneg_right          (mul_le_mul hcoeff hexpRHS (Real.exp_nonneg _) (by positivity)) hs_nn    _ = 1.41 / Real.sqrt 5.5666305 * s * Real.exp (-(1.5 / Real.sqrt 5.5666305) * s) := by ring