FKS2.corollary_14_normalized

theorem corollary_14_normalized :    Eθ.classicalBound 9.22023 (3 / 2) 0.8476 1 2 := by  intro x hx  have hθ := corollary_14 x hx  have hxpos : (0 : ℝ) < x := by linarith  have hlogpos : 0 < Real.log x := Real.log_pos (by linarith)  have hlognn : 0 ≤ Real.log x := hlogpos.le  have hsqrtpos : 0 ≤ Real.sqrt (Real.log x) := Real.sqrt_nonneg _  have hcoeff :      121.0961 / ((5.5666305 : ℝ) ^ (3 / 2 : ℝ)) ≤ 9.22023 := by    have hsqrt_lb : (2.35937 : ℝ) ≤ Real.sqrt 5.5666305 := by      calc (2.35937 : ℝ) = Real.sqrt ((2.35937 : ℝ) ^ 2) :=            (Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2.35937)).symm        _ ≤ Real.sqrt 5.5666305 := by            apply Real.sqrt_le_sqrt            norm_num    have hpow_base :        ((5.5666305 : ℝ) ^ (3 / 2 : ℝ)) = 5.5666305 * Real.sqrt 5.5666305 := by      rw [show (3 / 2 : ℝ) = 1 + (1 / 2 : ℝ) by norm_num,        Real.rpow_add (by norm_num : (0 : ℝ) < 5.5666305)]      simp [Real.sqrt_eq_rpow]    rw [hpow_base]    rw [div_le_iff₀ (by positivity : (0 : ℝ) < 5.5666305 * Real.sqrt 5.5666305)]    calc (121.0961 : ℝ)        ≤ 9.22023 * 5.5666305 * 2.35937 := by norm_num      _ ≤ 9.22023 * (5.5666305 * Real.sqrt 5.5666305) := by          nlinarith [hsqrt_lb]  have hC : (0.8476 : ℝ) ≤ 2 / Real.sqrt 5.5666305 := by    have hsqrt_ub : Real.sqrt 5.5666305 ≤ (2.3596 : ℝ) := by      calc Real.sqrt 5.5666305 ≤ Real.sqrt ((2.3596 : ℝ) ^ 2) := by            apply Real.sqrt_le_sqrt            norm_num        _ = (2.3596 : ℝ) := Real.sqrt_sq (by norm_num)    calc (0.8476 : ℝ)        ≤ 2 / (2.3596 : ℝ) := by            rw [le_div_iff₀ (by norm_num : (0 : ℝ) < 2.3596)]            norm_num      _ ≤ 2 / Real.sqrt 5.5666305 := by          gcongr  have hpow :      (Real.log x / 5.5666305) ^ (3 / 2 : ℝ) =        (Real.log x) ^ (3 / 2 : ℝ) / 5.5666305 ^ (3 / 2 : ℝ) := by    rw [Real.div_rpow hlognn (by norm_num : (0 : ℝ) ≤ 5.5666305)]  have hsqrt :      (Real.log x / 5.5666305) ^ ((1 : ℝ) / 2) =        Real.sqrt (Real.log x) / Real.sqrt 5.5666305 := by    rw [show ((1 : ℝ) / 2) = (1 / 2 : ℝ) by norm_num,      Real.div_rpow hlognn (by norm_num : (0 : ℝ) ≤ 5.5666305)]    simp [Real.sqrt_eq_rpow]  unfold admissible_bound at hθ ⊢  simp only [div_one]  rw [hpow, hsqrt] at hθ  have hpow_nonneg : 0 ≤ (Real.log x) ^ (3 / 2 : ℝ) :=    Real.rpow_nonneg hlognn _  have hExp :      Real.exp (-(2 * (Real.sqrt (Real.log x) / Real.sqrt 5.5666305))) ≤        Real.exp (-(0.8476 * (Real.log x) ^ ((1 : ℝ) / 2))) := by    apply Real.exp_le_exp.mpr    have hmul :        0.8476 * Real.sqrt (Real.log x) ≤          (2 / Real.sqrt 5.5666305) * Real.sqrt (Real.log x) :=      mul_le_mul_of_nonneg_right hC hsqrtpos    have hrewrite :        (2 / Real.sqrt 5.5666305) * Real.sqrt (Real.log x) =          2 * (Real.sqrt (Real.log x) / Real.sqrt 5.5666305) := by ring    rw [← Real.sqrt_eq_rpow]    nlinarith [hmul, hrewrite]  have hmul :      121.0961 * ((Real.log x) ^ (3 / 2 : ℝ) / 5.5666305 ^ (3 / 2 : ℝ)) *          Real.exp (-(2 * (Real.sqrt (Real.log x) / Real.sqrt 5.5666305))) ≤        9.22023 * (Real.log x) ^ (3 / 2 : ℝ) *          Real.exp (-(0.8476 * (Real.log x) ^ ((1 : ℝ) / 2))) := by    calc      121.0961 * ((Real.log x) ^ (3 / 2 : ℝ) / 5.5666305 ^ (3 / 2 : ℝ)) *          Real.exp (-(2 * (Real.sqrt (Real.log x) / Real.sqrt 5.5666305)))          = (121.0961 / 5.5666305 ^ (3 / 2 : ℝ)) *              (Real.log x) ^ (3 / 2 : ℝ) *              Real.exp (-(2 * (Real.sqrt (Real.log x) / Real.sqrt 5.5666305))) := by ring      _ ≤ 9.22023 * (Real.log x) ^ (3 / 2 : ℝ) *          Real.exp (-(0.8476 * (Real.log x) ^ ((1 : ℝ) / 2))) := by          gcongr  have hθ' :      Eθ x ≤ 121.0961 * ((Real.log x) ^ (3 / 2 : ℝ) / 5.5666305 ^ (3 / 2 : ℝ)) *          Real.exp (-(2 * (Real.sqrt (Real.log x) / Real.sqrt 5.5666305))) := by    convert! hθ using 1    ring_nf  convert! le_trans hθ' hmul using 1  ring_nf