FKS2.rowcurve_dom_two

lemma rowcurve_dom_two (A C coeff rate : ℝ) (x : ℝ)    (hL : (0:ℝ) ≤ Real.log x)    (hcoeff : coeff ≤ A / (5.5666305:ℝ) ^ (2:ℝ))    (hrate : C / Real.sqrt 5.5666305 ≤ rate)    (hcoeffnn : 0 ≤ coeff) :    coeff * (Real.sqrt (Real.log x) * Real.sqrt (Real.log x) * Real.sqrt (Real.log x)        * Real.sqrt (Real.log x))        * Real.exp (-rate * Real.sqrt (Real.log x))      ≤ admissible_bound A 2 C 5.5666305 x := by  rw [admissible_two_eq A C 5.5666305 x hL (by norm_num)]  set s := Real.sqrt (Real.log x) with hs_def  have hsnn : (0:ℝ) ≤ s := Real.sqrt_nonneg _  have hssss : s * s * s * s = s ^ 4 := by ring  have hAnn : (0:ℝ) ≤ A / (5.5666305:ℝ) ^ (2:ℝ) := le_trans hcoeffnn hcoeff  have hexpRHS : Real.exp (-rate * s) ≤ Real.exp (-(C / Real.sqrt 5.5666305) * s) := by    apply Real.exp_le_exp.mpr    have := mul_le_mul_of_nonneg_right hrate hsnn    simp only [neg_mul]; linarith  have hs4 : (0:ℝ) ≤ s ^ 4 := by positivity  rw [hssss]  calc coeff * s ^ 4 * Real.exp (-rate * s)      = (coeff * Real.exp (-rate * s)) * s ^ 4 := by ring    _ ≤ ((A / (5.5666305:ℝ) ^ (2:ℝ)) * Real.exp (-(C / Real.sqrt 5.5666305) * s)) * s ^ 4 :=        mul_le_mul_of_nonneg_right          (mul_le_mul hcoeff hexpRHS (Real.exp_nonneg _) hAnn) hs4    _ = A / (5.5666305:ℝ) ^ (2:ℝ) * s ^ 4 * Real.exp (-(C / Real.sqrt 5.5666305) * s) := by ring