FKS2.cor14_tail

theorem cor14_tail :    ∀ x ≥ exp 20000, Eπ x ≤ admissible_bound 121.107 1.5 2 5.5666305 x := by  have htail :=    theorem_3 121.0961 (3 / 2) 2 5.5666305 2 (exp 20000)      (by rw [ge_iff_le, max_le_iff]; constructor <;> norm_num)      (by norm_num)      corollary_14      (by rw [ge_iff_le, max_le_iff]          refine ⟨le_trans Real.exp_one_gt_two.le            (Real.exp_le_exp.mpr (by norm_num : (1:ℝ) ≤ 20000)), ?_⟩          apply Real.exp_le_exp.mpr          have h1 : (2:ℝ) / (2 * Real.sqrt 5.5666305) ≤ 1 := by            rw [div_le_iff₀ (by positivity)]; nlinarith [sqrtR5_lb]          have h0 : (0:ℝ) ≤ 2 / (2 * Real.sqrt 5.5666305) := by positivity          nlinarith [h1, h0])      (by norm_num)      (by norm_num)      (by norm_num)      (by have h1 : (2:ℝ) / (2 * Real.sqrt 5.5666305) ≤ 0.4239 := by            rw [div_le_iff₀ (by positivity)]; nlinarith [sqrtR5_lb]          have hlog2 : (0.6931471803 : ℝ) < Real.log 2 := Real.log_two_gt_d9          have hsq : (0.8325 : ℝ) ^ 2 ≤ Real.log 2 := by nlinarith [hlog2]          have hsqrt : (0.8325 : ℝ) ≤ Real.sqrt (Real.log 2) := by            calc (0.8325 : ℝ) = Real.sqrt ((0.8325 : ℝ) ^ 2) :=                  (Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 0.8325)).symm              _ ≤ Real.sqrt (Real.log 2) := Real.sqrt_le_sqrt hsq          linarith)  intro x hx  have hmain := htail x hx  rw [show (3 / 2 : ℝ) = 1.5 by norm_num] at hmain  have hμ : μ_asymp 121.0961 1.5 2 5.5666305 2 (exp 20000) ≤ 9e-5 := mu_asymp_num_le_cor14  have hA :      121.0961 * (1 + μ_asymp 121.0961 1.5 2 5.5666305 2 (exp 20000)) ≤ 121.107 := by    nlinarith [hμ]  refine le_trans hmain ?_  have hlognn : 0 ≤ Real.log x := by    have hx1 : (1 : ℝ) ≤ x := le_trans (by norm_num : (1 : ℝ) ≤ exp 20000) hx    exact Real.log_nonneg hx1  unfold admissible_bound  have hP : (0:ℝ) ≤ (Real.log x / 5.5666305) ^ (1.5:ℝ) :=    Real.rpow_nonneg (div_nonneg hlognn (by norm_num)) _  exact mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_right hA hP) (Real.exp_nonneg _)