FKS2.rhsE2_row1_le_sq

theorem rhsE2_row1_le_sq (x : ℝ) (hL : (22.955 : ℝ) ≤ Real.log x) :    Expr.eval (fun _ => Real.sqrt (Real.log x)) rhsE2_row1      ≤ (admissible_bound 0.000120 0.25 1 5.5666305 x) ^ 2 := by  have hLnn : (0:ℝ) ≤ Real.log x := by linarith  rw [eval_rhsE2_row1, admissible_quarter_eq 0.000120 1 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_ub := sqrtR5_ub  have hsqrtR_pos := sqrtR5_pos  have hsqs : (Real.sqrt s) ^ 2 = s := Real.sq_sqrt hs_nn  have hexp2 : (Real.exp (-(1 / Real.sqrt 5.5666305) * s)) ^ 2      = Real.exp (-(2 / Real.sqrt 5.5666305) * s) := by    rw [← Real.exp_nat_mul]; congr 1; push_cast; ring  have hexpand : (0.000120 / (5.5666305:ℝ)^((1:ℝ)/4) * Real.sqrt s        * Real.exp (-(1 / Real.sqrt 5.5666305) * s)) ^ 2      = (0.000120 / (5.5666305:ℝ)^((1:ℝ)/4))^2 * s * Real.exp (-(2 / Real.sqrt 5.5666305) * s) := by    rw [mul_pow, mul_pow, hsqs, hexp2]  rw [hexpand]  have hR14sq : ((5.5666305:ℝ)^((1:ℝ)/4))^2 = Real.sqrt 5.5666305 := by    rw [← Real.rpow_natCast ((5.5666305:ℝ)^((1:ℝ)/4)) 2, ← Real.rpow_mul (by norm_num),      Real.sqrt_eq_rpow]; norm_num  have hcoeff : (6102/1000000000000:ℝ) ≤ (0.000120 / (5.5666305:ℝ)^((1:ℝ)/4))^2 := by    rw [div_pow, hR14sq, le_div_iff₀ hsqrtR_pos,      show (0.000120:ℝ)^2 = 144/10000000000 by norm_num]    nlinarith [hsqrtR_ub]  have hrate : (2:ℝ) / Real.sqrt 5.5666305 ≤ 8477/10000 := by    rw [div_le_iff₀ hsqrtR_pos]; nlinarith [sqrtR5_lb]  have hexpRHS : Real.exp (-(8477/10000:ℝ) * s) ≤ Real.exp (-(2 / Real.sqrt 5.5666305) * s) := by    apply Real.exp_le_exp.mpr    have : (2 / Real.sqrt 5.5666305) * s ≤ (8477/10000) * s := mul_le_mul_of_nonneg_right hrate hs_nn    simp only [neg_mul]; linarith  calc (6102/1000000000000:ℝ) * s * Real.exp (-(8477/10000) * s)      = ((6102/1000000000000:ℝ) * Real.exp (-(8477/10000) * s)) * s := by ring    _ ≤ ((0.000120 / (5.5666305:ℝ)^((1:ℝ)/4))^2 * Real.exp (-(2 / Real.sqrt 5.5666305) * s)) * s :=        mul_le_mul_of_nonneg_right          (mul_le_mul hcoeff hexpRHS (Real.exp_nonneg _) (by positivity)) hs_nn    _ = (0.000120 / (5.5666305:ℝ)^((1:ℝ)/4))^2 * s * Real.exp (-(2 / Real.sqrt 5.5666305) * s) := by ring