FKS2.admissible_bound_anti

lemma admissible_bound_anti {A C x y : ℝ} (hA : 0 ≤ A) (hC : 0 < C)    (hx : (3 / C) ^ 2 ≤ Real.log x) (hxy : x ≤ y) (hx0 : 0 < x) :    admissible_bound A 1.5 C 1 y ≤ admissible_bound A 1.5 C 1 x := by  unfold admissible_bound  rw [div_one, div_one]  have hLx : (0:ℝ) ≤ Real.log x := le_trans (by positivity) hx  have hLxy : Real.log x ≤ Real.log y :=    Real.log_le_log hx0 hxy  have hLy : (0:ℝ) ≤ Real.log y := le_trans hLx hLxy  -- rewrite both sides through t = √(log ·)  have key : ∀ L : ℝ, 0 ≤ L →      A * L ^ (1.5:ℝ) * Real.exp (-C * L ^ ((1:ℝ)/(2:ℝ))) =        A * (Real.sqrt L) ^ 3 * Real.exp (-C * Real.sqrt L) := by    intro L hL    rw [Real.sqrt_eq_rpow, ← Real.rpow_natCast (L ^ ((1:ℝ)/2)) 3,      ← Real.rpow_mul hL]    norm_num  rw [key _ hLx, key _ hLy]  have htx : 3 / C ≤ Real.sqrt (Real.log x) := by    have h := Real.sqrt_le_sqrt hx    rwa [Real.sqrt_sq (by positivity : (0:ℝ) ≤ 3 / C)] at h  have hty : Real.sqrt (Real.log x) ≤ Real.sqrt (Real.log y) :=    Real.sqrt_le_sqrt hLxy  exact cube_mul_exp_antitoneOn hA hC    (Set.mem_Ici.mpr htx) (Set.mem_Ici.mpr (le_trans htx hty)) hty