FKS2.tail_row2

theorem tail_row2 : ∀ x ≥ exp (20000:ℝ),    Eπ x ≤ admissible_bound 0.826 0.25 1 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_quarter_eq 0.826 1 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  have hsqrts_ge1 : (1:ℝ) ≤ Real.sqrt s := by    rw [show (1:ℝ) = Real.sqrt 1 from Real.sqrt_one.symm]    exact Real.sqrt_le_sqrt (by linarith)  have hcoeffLB : (0.5377:ℝ) ≤ 0.826 / (5.5666305:ℝ) ^ ((1:ℝ)/4) := by    rw [le_div_iff₀ (Real.rpow_pos_of_pos (by norm_num) _)]; nlinarith [R5_rpow_quarter_le]  have hCR : (1:ℝ) / Real.sqrt 5.5666305 ≤ 0.4239 := by    rw [div_le_iff₀ hsqrtR_pos]; nlinarith [hsqrtR_lb]  have hexpRHS : Real.exp (-(0.4239:ℝ) * s) ≤ Real.exp (-(1 / Real.sqrt 5.5666305) * s) := by    apply Real.exp_le_exp.mpr    have : (1 / Real.sqrt 5.5666305) * s ≤ 0.4239 * s := mul_le_mul_of_nonneg_right hCR hs_nn    simp only [neg_mul]; linarith  -- cube bound: 9.2211·s³·e^{-0.8476 s} ≤ 0.5377·e^{-0.4239 s}  have hcube : (9.2211:ℝ) * s^3 * Real.exp (-(0.8476) * s) ≤ 0.5377 * Real.exp (-(0.4239) * s) := by    have hlin : s * Real.exp (-(0.05:ℝ) * s) ≤ 20 * Real.exp (-1) := by      have hab : (0.05:ℝ) * s ≤ Real.exp (0.05 * s - 1) := by        have := Real.add_one_le_exp (0.05 * s - 1); linarith      have h := mul_le_mul_of_nonneg_right hab (Real.exp_nonneg (-(0.05 * s)))      rw [← Real.exp_add] at h      have he : (0.05 * s - 1) + -(0.05 * s) = -1 := by ring      rw [he] at h      have heq : (-(0.05:ℝ) * s) = -(0.05*s) := by ring      rw [heq]; nlinarith [h, Real.exp_nonneg (-(0.05*s))]    have hcube3 : s^3 * Real.exp (-(0.15:ℝ) * s) ≤ 8000 * Real.exp (-3) := by      have hpow : (Real.exp (-(0.05:ℝ) * s))^(3:ℕ) = Real.exp (-(0.15) * s) := by        rw [← Real.exp_nat_mul]; congr 1; push_cast; ring      have hfac : s^3 * Real.exp (-(0.15:ℝ) * s) = (s * Real.exp (-(0.05) * s))^(3:ℕ) := by        rw [mul_pow, hpow]      rw [hfac]      have hnn : (0:ℝ) ≤ s * Real.exp (-(0.05) * s) := by positivity      calc (s * Real.exp (-(0.05) * s))^(3:ℕ)          ≤ (20 * Real.exp (-1))^(3:ℕ) := by apply pow_le_pow_left₀ hnn hlin        _ = 8000 * Real.exp (-3) := by            rw [mul_pow, show ((20:ℝ))^(3:ℕ) = 8000 by norm_num]; congr 1            rw [← Real.exp_nat_mul]; congr 1; push_cast; ring    have hsplit : Real.exp (-(0.8476:ℝ) * s)        = Real.exp (-(0.15) * s) * (Real.exp (-(0.2737) * s) * Real.exp (-(0.4239) * s)) := by      rw [← Real.exp_add, ← Real.exp_add]; congr 1; ring    have htail12 : Real.exp (-(0.2737:ℝ) * s) ≤ Real.exp (-12) := by      apply Real.exp_le_exp.mpr; nlinarith [hs141]    have hexp15 : (137200:ℝ) ≤ Real.exp 15 := by      have he : Real.exp 15 = (Real.exp 1) ^ (15:ℕ) := by rw [← Real.exp_nat_mul]; norm_num      rw [he]      calc (137200:ℝ) ≤ (2.7:ℝ)^(15:ℕ) := by norm_num        _ ≤ (Real.exp 1)^(15:ℕ) := by gcongr; linarith [Real.exp_one_gt_d9]    rw [hsplit,      show (9.2211:ℝ) * s^3 * (Real.exp (-(0.15)*s) * (Real.exp (-(0.2737)*s) * Real.exp (-(0.4239)*s)))        = 9.2211 * (s^3 * Real.exp (-(0.15)*s)) * Real.exp (-(0.2737)*s) * Real.exp (-(0.4239)*s) by ring]    have hstep : (9.2211:ℝ) * (s^3 * Real.exp (-(0.15)*s)) * Real.exp (-(0.2737)*s)        ≤ 9.2211 * (8000 * Real.exp (-3)) * Real.exp (-12) := by      apply mul_le_mul _ htail12 (Real.exp_nonneg _) (by positivity)      exact mul_le_mul_of_nonneg_left hcube3 (by norm_num)    have hfinal : (9.2211:ℝ) * (8000 * Real.exp (-3)) * Real.exp (-12) ≤ 0.5377 := by      rw [show (9.2211:ℝ) * (8000 * Real.exp (-3)) * Real.exp (-12) = 73768.8 * Real.exp (-15) by        rw [show (-15:ℝ) = -3 + -12 by ring, Real.exp_add]; ring]      rw [Real.exp_neg, mul_inv_le_iff₀ (Real.exp_pos _)]; nlinarith [hexp15]    calc (9.2211:ℝ) * (s^3 * Real.exp (-(0.15)*s)) * Real.exp (-(0.2737)*s) * Real.exp (-(0.4239)*s)        ≤ (9.2211 * (8000 * Real.exp (-3)) * Real.exp (-12)) * Real.exp (-(0.4239)*s) :=          mul_le_mul_of_nonneg_right hstep (Real.exp_nonneg _)      _ ≤ 0.5377 * Real.exp (-(0.4239)*s) := mul_le_mul_of_nonneg_right hfinal (Real.exp_nonneg _)  -- assemble: LHS ≤ 0.5377·e^{-0.4239s} ≤ coeff·√s·e^{-(1/√R)s}  calc (9.2211:ℝ) * s^3 * Real.exp (-(0.8476) * s)      ≤ 0.5377 * Real.exp (-(0.4239) * s) := hcube    _ ≤ 0.826 / (5.5666305:ℝ)^((1:ℝ)/4) * Real.sqrt s * Real.exp (-(1 / Real.sqrt 5.5666305) * s) := by        have hRHSnn : (0:ℝ) ≤ 0.826 / (5.5666305:ℝ)^((1:ℝ)/4) := by positivity        calc (0.5377:ℝ) * Real.exp (-(0.4239)*s)            ≤ 0.826 / (5.5666305:ℝ)^((1:ℝ)/4) * Real.exp (-(0.4239)*s) :=              mul_le_mul_of_nonneg_right hcoeffLB (Real.exp_nonneg _)          _ ≤ 0.826 / (5.5666305:ℝ)^((1:ℝ)/4) * Real.sqrt s * Real.exp (-(0.4239)*s) := by              rw [mul_assoc]              apply mul_le_mul_of_nonneg_left _ hRHSnn              calc Real.exp (-(0.4239)*s) = 1 * Real.exp (-(0.4239)*s) := (one_mul _).symm                _ ≤ Real.sqrt s * Real.exp (-(0.4239)*s) :=                    mul_le_mul_of_nonneg_right hsqrts_ge1 (Real.exp_nonneg _)          _ ≤ 0.826 / (5.5666305:ℝ)^((1:ℝ)/4) * Real.sqrt s * Real.exp (-(1 / Real.sqrt 5.5666305) * s) := by              apply mul_le_mul_of_nonneg_left hexpRHS (by positivity)