FKS2.tail_row3

theorem tail_row3 : ∀ x ≥ exp (20000:ℝ),    Eπ x ≤ admissible_bound 1.41 0.5 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_half_eq 1.41 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_ub := sqrtR5_ub  have hsqrtR_pos := sqrtR5_pos  have hCR : (1.5:ℝ) / Real.sqrt 5.5666305 ≤ 0.63577 := by    rw [div_le_iff₀ hsqrtR_pos]; nlinarith [hsqrtR_lb]  have hexpRHS : Real.exp (-(0.63577:ℝ) * s) ≤ Real.exp (-(1.5 / Real.sqrt 5.5666305) * s) := by    apply Real.exp_le_exp.mpr    have : (1.5 / Real.sqrt 5.5666305) * s ≤ 0.63577 * s := mul_le_mul_of_nonneg_right hCR hs_nn    simp only [neg_mul]; linarith  have hcoeffLB : (0.5976:ℝ) ≤ 1.41 / Real.sqrt 5.5666305 := by    rw [le_div_iff₀ hsqrtR_pos]; nlinarith [hsqrtR_ub]  have hcentral : (9.2211:ℝ) * (s*s) * Real.exp (-(0.21183) * s) ≤ 0.5976 := 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 hh2 : (Real.exp (-(0.05:ℝ) * s))^(2:ℕ) = Real.exp (-(0.1) * s) := by      rw [← Real.exp_nat_mul]; congr 1; push_cast; ring    have hsq : (s*s) * Real.exp (-(0.1:ℝ) * s) ≤ 400 * Real.exp (-2) := by      have hfac : (s*s) * Real.exp (-(0.1:ℝ) * s) = (s * Real.exp (-(0.05) * s))^(2:ℕ) := by        rw [mul_pow, hh2]; ring      rw [hfac]      have hnn : (0:ℝ) ≤ s * Real.exp (-(0.05) * s) := by positivity      calc (s * Real.exp (-(0.05) * s))^(2:ℕ)          ≤ (20 * Real.exp (-1))^(2:ℕ) := by apply pow_le_pow_left₀ hnn hlin        _ = 400 * Real.exp (-2) := by            rw [mul_pow, show ((20:ℝ))^(2:ℕ) = 400 by norm_num]            congr 1            rw [← Real.exp_nat_mul]; congr 1; push_cast; ring    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 htail9 : Real.exp (-(0.11183:ℝ) * s) ≤ Real.exp (-9) := by      apply Real.exp_le_exp.mpr; nlinarith [hs141]    have hexp11 : (50000:ℝ) ≤ Real.exp 11 := by      have he : Real.exp 11 = (Real.exp 1) ^ (11:ℕ) := by rw [← Real.exp_nat_mul]; norm_num      rw [he]      calc (50000:ℝ) ≤ (2.7:ℝ)^(11:ℕ) := by norm_num        _ ≤ (Real.exp 1)^(11:ℕ) := by gcongr; linarith [Real.exp_one_gt_d9]    rw [hsplit, show (9.2211:ℝ) * (s*s) * (Real.exp (-(0.1)*s) * Real.exp (-(0.11183)*s))        = 9.2211 * ((s*s) * Real.exp (-(0.1)*s)) * Real.exp (-(0.11183)*s) by ring]    have hstep : (9.2211:ℝ) * ((s*s) * Real.exp (-(0.1)*s)) * Real.exp (-(0.11183)*s)        ≤ 9.2211 * (400 * Real.exp (-2)) * Real.exp (-9) := by      apply mul_le_mul      · exact mul_le_mul_of_nonneg_left hsq (by norm_num)      · exact htail9      · exact Real.exp_nonneg _      · positivity    refine le_trans hstep ?_    have hcomb : (9.2211:ℝ) * (400 * Real.exp (-2)) * Real.exp (-9) = 3688.44 * Real.exp (-11) := by      rw [show (-11:ℝ) = -2 + -9 by ring, Real.exp_add]; ring    rw [hcomb, Real.exp_neg, mul_inv_le_iff₀ (Real.exp_pos _)]    nlinarith [hexp11]  have hs3eq : s^3 = (s*s)*s := by ring  have hLHS : (9.2211:ℝ) * s^3 * Real.exp (-(0.8476) * s)      = (9.2211 * (s*s) * Real.exp (-(0.21183) * s)) * (s * Real.exp (-(0.63577) * s)) := by    rw [hs3eq, show -(0.8476:ℝ)*s = -(0.21183)*s + -(0.63577)*s by ring, Real.exp_add]; ring  have hfac_nn : (0:ℝ) ≤ s * Real.exp (-(0.63577) * s) := by positivity  calc (9.2211:ℝ) * s^3 * Real.exp (-(0.8476) * s)      = (9.2211 * (s*s) * Real.exp (-(0.21183) * s)) * (s * Real.exp (-(0.63577) * s)) := hLHS    _ ≤ 0.5976 * (s * Real.exp (-(0.63577) * s)) := mul_le_mul_of_nonneg_right hcentral hfac_nn    _ ≤ (1.41 / Real.sqrt 5.5666305) * s * Real.exp (-(1.5 / Real.sqrt 5.5666305) * s) := by        have h1 : (0.5976:ℝ) * (s * Real.exp (-(0.63577) * s))            ≤ (1.41 / Real.sqrt 5.5666305) * (s * Real.exp (-(0.63577) * s)) :=          mul_le_mul_of_nonneg_right hcoeffLB hfac_nn        have h2 : (1.41 / Real.sqrt 5.5666305) * (s * Real.exp (-(0.63577) * s))            ≤ (1.41 / Real.sqrt 5.5666305) * (s * 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 hexpRHS hs_nn        calc (0.5976:ℝ) * (s * Real.exp (-(0.63577) * s))            ≤ (1.41 / Real.sqrt 5.5666305) * (s * Real.exp (-(0.63577) * s)) := h1          _ ≤ (1.41 / Real.sqrt 5.5666305) * (s * Real.exp (-(1.5 / Real.sqrt 5.5666305) * s)) := h2          _ = (1.41 / Real.sqrt 5.5666305) * s * Real.exp (-(1.5 / Real.sqrt 5.5666305) * s) := by ring