FKS2.tail_row4

theorem tail_row4 : ∀ x ≥ exp (20000:ℝ),    Eπ x ≤ admissible_bound 1.76 1 1.5 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_one_eq 1.76 1.5 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 hsqrtR_lb := sqrtR5_lb  have hsqrtR_pos := sqrtR5_pos  -- rate bound: 1.5/√R ≤ 0.63577  have hCR : (1.5:ℝ) / Real.sqrt 5.5666305 ≤ 0.63577 := by    rw [div_le_iff₀ hsqrtR_pos]; nlinarith [hsqrtR_lb]  -- coefficient lower bound: 0.316 ≤ 1.76/R  have hcoeff : (0.316:ℝ) ≤ 1.76 / (5.5666305:ℝ) := by    rw [le_div_iff₀ (by norm_num)]; norm_num  -- central scalar bound: 9.2211·s·e^{-0.21183 s} ≤ 0.316  (uses s ≥ 141)  have hcentral : (9.2211:ℝ) * s * Real.exp (-(0.21183) * s) ≤ 0.316 := by    have hsplit : Real.exp (-(0.21183:ℝ) * s)        = Real.exp (-(0.1) * s) * Real.exp (-(0.11183) * s) := by      rw [← Real.exp_add]; congr 1; ring    have hpoly : s * Real.exp (-(0.1:ℝ) * s) ≤ 10 * Real.exp (-1) := by      have hab : (0.1:ℝ) * s ≤ Real.exp (0.1 * s - 1) := by        have := Real.add_one_le_exp (0.1 * s - 1); linarith      have h := mul_le_mul_of_nonneg_right hab (Real.exp_nonneg (-(0.1 * s)))      rw [← Real.exp_add] at h      have he : (0.1 * s - 1) + -(0.1 * s) = -1 := by ring      rw [he] at h      have heq : (-(0.1:ℝ) * s) = -(0.1*s) := by ring      rw [heq]      nlinarith [h, Real.exp_nonneg (-(0.1*s))]    have htail6 : Real.exp (-(0.11183:ℝ) * s) ≤ Real.exp (-6) := by      apply Real.exp_le_exp.mpr      nlinarith [hs141]    have hexp7 : (1000:ℝ) ≤ Real.exp 7 := by      have h1 : (2.7:ℝ) ≤ Real.exp 1 := by linarith [Real.exp_one_gt_d9]      have he : Real.exp 7 = Real.exp 1 ^ (7:ℕ) := by rw [← Real.exp_nat_mul]; norm_num      rw [he]      calc (1000:ℝ) ≤ (2.7:ℝ)^(7:ℕ) := by norm_num        _ ≤ Real.exp 1 ^ (7:ℕ) := by gcongr    have hexpneg7 : Real.exp (-7) ≤ 1/1000 := by      rw [Real.exp_neg, inv_eq_one_div]      exact one_div_le_one_div_of_le (by norm_num) hexp7    rw [hsplit]    have hstep : (9.2211:ℝ) * s * (Real.exp (-(0.1) * s) * Real.exp (-(0.11183) * s))        ≤ 9.2211 * (10 * Real.exp (-1)) * Real.exp (-6) := by      have h1 : (9.2211:ℝ) * s * (Real.exp (-(0.1)*s) * Real.exp (-(0.11183)*s))          = 9.2211 * (s * Real.exp (-(0.1)*s)) * Real.exp (-(0.11183)*s) := by ring      rw [h1]      apply mul_le_mul      · exact mul_le_mul_of_nonneg_left hpoly (by norm_num)      · exact htail6      · exact Real.exp_nonneg _      · positivity    refine le_trans hstep ?_    have hcomb : (9.2211:ℝ) * (10 * Real.exp (-1)) * Real.exp (-6) = 92.211 * Real.exp (-7) := by      rw [show (-7:ℝ) = -1 + -6 by ring, Real.exp_add]; ring    rw [hcomb]    nlinarith [hexpneg7, Real.exp_pos (-7:ℝ)]  -- assemble: rewrite the exponential gap, factor s³ = s·s², dominate  have hs2_nn : (0:ℝ) ≤ s ^ 2 := by positivity  have hexp_gap : Real.exp (-(0.63577:ℝ) * s)      ≤ Real.exp (-(1.5 / Real.sqrt 5.5666305) * s) := by    apply Real.exp_le_exp.mpr    have hCRs : (1.5 / Real.sqrt 5.5666305) * s ≤ 0.63577 * s :=      mul_le_mul_of_nonneg_right hCR hs_nn    simp only [neg_mul]; linarith [hCRs]  have hLHS : (9.2211:ℝ) * s ^ 3 * Real.exp (-(0.8476) * s)      = (9.2211 * s * Real.exp (-(0.21183) * s)) * (s ^ 2 * Real.exp (-(0.63577) * s)) := by    rw [show (-(0.8476:ℝ)) * s = (-(0.21183) * s) + (-(0.63577) * s) by ring, Real.exp_add]    ring  calc (9.2211:ℝ) * s ^ 3 * Real.exp (-(0.8476) * s)      = (9.2211 * s * Real.exp (-(0.21183) * s)) * (s ^ 2 * Real.exp (-(0.63577) * s)) := hLHS    _ ≤ 0.316 * (s ^ 2 * Real.exp (-(0.63577) * s)) := by        apply mul_le_mul_of_nonneg_right hcentral        positivity    _ ≤ (1.76 / 5.5666305) * s ^ 2 * Real.exp (-(1.5 / Real.sqrt 5.5666305) * s) := by        have h1 : (0.316:ℝ) * (s ^ 2 * Real.exp (-(0.63577) * s))            ≤ (1.76 / 5.5666305) * (s ^ 2 * Real.exp (-(0.63577) * s)) := by          apply mul_le_mul_of_nonneg_right hcoeff          positivity        have h2 : (1.76 / 5.5666305 : ℝ) * (s ^ 2 * Real.exp (-(0.63577) * s))            ≤ (1.76 / 5.5666305) * (s ^ 2 * Real.exp (-(1.5 / Real.sqrt 5.5666305) * s)) := by          apply mul_le_mul_of_nonneg_left _ (by positivity)          exact mul_le_mul_of_nonneg_left hexp_gap hs2_nn        calc (0.316:ℝ) * (s ^ 2 * Real.exp (-(0.63577) * s))            ≤ (1.76 / 5.5666305) * (s ^ 2 * Real.exp (-(0.63577) * s)) := h1          _ ≤ (1.76 / 5.5666305) * (s ^ 2 * Real.exp (-(1.5 / Real.sqrt 5.5666305) * s)) := h2          _ = (1.76 / 5.5666305) * s ^ 2 * Real.exp (-(1.5 / Real.sqrt 5.5666305) * s) := by ring