FKS2.corollary_22_tail

theorem corollary_22_tail :    ∀ x ≥ exp 20000, Eπ x ≤ admissible_bound 9.2211 (3 / 2) 0.8476 1 x := by  have htail :=    theorem_3 9.22023 (3 / 2) 0.8476 1 2 (exp 20000)      (by norm_num)      (by norm_num)      corollary_14_normalized      (by        rw [ge_iff_le, max_le_iff]        constructor        · exact le_trans Real.exp_one_gt_two.le            (Real.exp_le_exp.mpr (by norm_num : (1 : ℝ) ≤ 20000))        · apply Real.exp_le_exp.mpr          rw [Real.sqrt_one]          norm_num)      (by norm_num)      (by norm_num)      (by norm_num)      (by        rw [Real.sqrt_one]        have hlog2 : (0.6931471803 : ℝ) < Real.log 2 := Real.log_two_gt_d9        have hsq : (0.8325 : ℝ) ^ 2 ≤ Real.log 2 := by          norm_num          linarith        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 hμ : μ_asymp 9.22023 1.5 0.8476 1 2 (exp 20000) ≤ 5.01516e-5 :=    mu_asymp_num_le (by norm_num : (1 : ℝ) ≤ 9.22023)  have hA :      9.22023 * (1 + μ_asymp 9.22023 (3 / 2) 0.8476 1 2 (exp 20000)) ≤        9.2211 := by    have hμ' : μ_asymp 9.22023 (3 / 2) 0.8476 1 2 (exp 20000) ≤ 5.01516e-5 := by      norm_num at hμ ⊢      exact hμ    nlinarith [hμ']  have hmain := htail x hx  unfold admissible_bound at hmain ⊢  rw [div_one] at hmain ⊢  have hlognn : 0 ≤ Real.log x := by    have hx1 : (1 : ℝ) ≤ x := by      exact le_trans (by norm_num : (1 : ℝ) ≤ exp 20000) hx    exact Real.log_nonneg hx1  have hpow_nonneg : 0 ≤ (Real.log x) ^ (3 / 2 : ℝ) :=    Real.rpow_nonneg hlognn _  have hexp_nonneg : 0 ≤ Real.exp (-(0.8476 * (Real.log x) ^ ((1 : ℝ) / 2))) :=    Real.exp_nonneg _  exact le_trans hmain (by gcongr)