FaberKadiri.psi_bound

@[blueprint  "thm:faber-kadiri-psi"  (title := "Faber--Kadiri Corollary 1.2")  (statement := /-- For $x \geq e^{20}$, we have $|\psi(x) - x| \leq 5.3688\cdot 10^{-4}\, x$.    (Following \cite{faber-kadiri}, Corollary~1.2.  The Lean hypothesis uses the    integer threshold $485{,}165{,}196=\lceil e^{20}\rceil$.) -/)  (latexEnv := "theorem")]theorem psi_bound (x : ℝ) (hx : x ≥ 485165196) :    |ψ x - x| ≤ 5.3688e-4 * x := by  have hx_pos : (0 : ℝ) < x := by linarith  have hmem : (4, (59.18 : ℝ)) ∈ Dusart.Table_3_3 := by simp [Dusart.Table_3_3]  have hEpsi := Dusart.theorem_3_3 hmem (show x ≥ 2 by linarith)  rw [show Eψ x = |ψ x - x| / x from rfl] at hEpsi  rw [div_le_iff₀ hx_pos] at hEpsi  apply hEpsi.trans (mul_le_mul_of_nonneg_right _ hx_pos.le)  have hlog : (20 : ℝ) ≤ log x := by    rw [le_log_iff_exp_le hx_pos]    exact LogTables.exp_20_le.trans hx  calc (59.18 : ℝ) / (log x) ^ 4      ≤ 59.18 / 20 ^ 4 := div_le_div_of_nonneg_left (by norm_num) (by norm_num)          (pow_le_pow_left₀ (by linarith) hlog 4)      _ ≤ 5.3688e-4 := by norm_num