FKS2.tail_three_halves_of

theorem tail_three_halves_of (A C rateUB coeffLB : ℝ)    (hrate : C / Real.sqrt 5.5666305 ≤ rateUB)    (hcoef : coeffLB ≤ A / (5.5666305:ℝ) ^ (1.5:ℝ))    (hgap : (0:ℝ) ≤ 0.8476 - rateUB)    (hkey : (9.2211:ℝ) ≤ coeffLB * Real.exp ((0.8476 - rateUB) * 141)) :    ∀ x ≥ exp (20000:ℝ), Eπ x ≤ admissible_bound A 1.5 C 5.5666305 x := by  intro x hx  have he2 : (2:ℝ) ≤ Real.exp 20000 := by    have := Real.add_one_le_exp (20000:ℝ); linarith  have hx2 : (2:ℝ) ≤ x := le_trans he2 hx  have hcor := corollary_22 x hx2  refine le_trans hcor ?_  have hL : (20000:ℝ) ≤ Real.log x := by    rw [← Real.log_exp 20000]; exact Real.log_le_log (Real.exp_pos _) hx  have hLnn : (0:ℝ) ≤ Real.log x := le_trans (by norm_num) hL  rw [admissible_three_halves_eq 9.2211 0.8476 1 x hLnn (by norm_num),      admissible_three_halves_eq A C 5.5666305 x hLnn (by norm_num)]  rw [show (1:ℝ) ^ (1.5:ℝ) = 1 by norm_num, Real.sqrt_one]  simp only [div_one]  set s := Real.sqrt (Real.log x) with hs_def  have hs_nn : (0:ℝ) ≤ s := Real.sqrt_nonneg _  have hs141 : (141:ℝ) ≤ s := by    rw [hs_def, show (141:ℝ) = Real.sqrt (141^2) from (Real.sqrt_sq (by norm_num)).symm]    exact Real.sqrt_le_sqrt (by nlinarith [hL])  have hs3 : (0:ℝ) ≤ s ^ 3 := by positivity  have hcoefnn : (0:ℝ) ≤ coeffLB := by    by_contra h; rw [not_le] at h    have := mul_neg_of_neg_of_pos h (Real.exp_pos ((0.8476 - rateUB) * 141))    linarith [hkey]  have hexpRHS : Real.exp (-rateUB * s) ≤ Real.exp (-(C / Real.sqrt 5.5666305) * s) := by    apply Real.exp_le_exp.mpr    have : (C / Real.sqrt 5.5666305) * s ≤ rateUB * s := mul_le_mul_of_nonneg_right hrate hs_nn    simp only [neg_mul]; linarith  have hkeyS : (9.2211:ℝ) * Real.exp (-(0.8476 - rateUB) * s) ≤ coeffLB := by    have hmono : Real.exp (-(0.8476 - rateUB) * s) ≤ Real.exp (-(0.8476 - rateUB) * 141) := by      apply Real.exp_le_exp.mpr      have : (0.8476 - rateUB) * 141 ≤ (0.8476 - rateUB) * s := mul_le_mul_of_nonneg_left hs141 hgap      simp only [neg_mul]; linarith    have hfromkey : (9.2211:ℝ) * Real.exp (-(0.8476 - rateUB) * 141) ≤ coeffLB := by      have := mul_le_mul_of_nonneg_right hkey (Real.exp_nonneg (-(0.8476 - rateUB) * 141))      rwa [mul_assoc, ← Real.exp_add,        show (0.8476 - rateUB) * 141 + -(0.8476 - rateUB) * 141 = 0 by ring,        Real.exp_zero, mul_one] at this    calc (9.2211:ℝ) * Real.exp (-(0.8476 - rateUB) * s)        ≤ 9.2211 * Real.exp (-(0.8476 - rateUB) * 141) :=          mul_le_mul_of_nonneg_left hmono (by norm_num)      _ ≤ coeffLB := hfromkey  have hscalar : (9.2211:ℝ) * Real.exp (-(0.8476) * s) ≤ coeffLB * Real.exp (-rateUB * s) := by    have hsplit : Real.exp (-(0.8476:ℝ) * s)        = Real.exp (-(0.8476 - rateUB) * s) * Real.exp (-rateUB * s) := by      rw [← Real.exp_add]; congr 1; ring    rw [hsplit, show (9.2211:ℝ) * (Real.exp (-(0.8476 - rateUB) * s) * Real.exp (-rateUB * s))        = (9.2211 * Real.exp (-(0.8476 - rateUB) * s)) * Real.exp (-rateUB * s) by ring]    exact mul_le_mul_of_nonneg_right hkeyS (Real.exp_nonneg _)  calc (9.2211:ℝ) * s ^ 3 * Real.exp (-(0.8476) * s)      = (9.2211 * Real.exp (-(0.8476) * s)) * s ^ 3 := by ring    _ ≤ (coeffLB * Real.exp (-rateUB * s)) * s ^ 3 := mul_le_mul_of_nonneg_right hscalar hs3    _ ≤ (coeffLB * Real.exp (-(C / Real.sqrt 5.5666305) * s)) * s ^ 3 := by        apply mul_le_mul_of_nonneg_right _ hs3        exact mul_le_mul_of_nonneg_left hexpRHS hcoefnn    _ ≤ ((A / (5.5666305:ℝ) ^ (1.5:ℝ)) * Real.exp (-(C / Real.sqrt 5.5666305) * s)) * s ^ 3 := by        apply mul_le_mul_of_nonneg_right _ hs3        exact mul_le_mul_of_nonneg_right hcoef (Real.exp_nonneg _)    _ = A / (5.5666305:ℝ) ^ (1.5:ℝ) * s ^ 3 * Real.exp (-(C / Real.sqrt 5.5666305) * s) := by ring