FKS2.rhsE2_le_rowcurve_sq

theorem rhsE2_le_rowcurve_sq (x : ℝ) (hL : (6 : ℝ) ≤ Real.log x) :    Expr.eval (fun _ => Real.sqrt (Real.log x)) rhsE2      ≤ (admissible_bound 0.826 0.25 1 5.5666305 x) ^ 2 := by  have hLnn : (0:ℝ) ≤ Real.log x := by linarith  rw [eval_rhsE2, admissible_quarter_eq 0.826 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  -- expand the square: ((0.826/R^{1/4})·√s·exp(−(1/√R)s))² = (0.826/R^{1/4})²·s·exp(−(2/√R)s)  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.826 / (5.5666305:ℝ)^((1:ℝ)/4) * Real.sqrt s        * Real.exp (-(1 / Real.sqrt 5.5666305) * s)) ^ 2      = (0.826 / (5.5666305:ℝ)^((1:ℝ)/4))^2 * s * Real.exp (-(2 / Real.sqrt 5.5666305) * s) := by    rw [mul_pow, mul_pow, hsqs, hexp2]  rw [hexpand]  -- coeff: 2891/10000 ≤ (0.826/R^{1/4})² = 0.826²/√R  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 : (2891/10000:ℝ) ≤ (0.826 / (5.5666305:ℝ)^((1:ℝ)/4))^2 := by    rw [div_pow, hR14sq, le_div_iff₀ hsqrtR_pos]; nlinarith [hsqrtR_ub]  -- rate: 2/√R ≤ 8477/10000  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 (2891/10000:ℝ) * s * Real.exp (-(8477/10000) * s)      = ((2891/10000:ℝ) * Real.exp (-(8477/10000) * s)) * s := by ring    _ ≤ ((0.826 / (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.826 / (5.5666305:ℝ)^((1:ℝ)/4))^2 * s * Real.exp (-(2 / Real.sqrt 5.5666305) * s) := by ring