Dusart1999.theorem_a

@[blueprint  "thm:dusart1999-a"  (title := "Dusart 1999, part a")  (statement := /-- For $x \geq e^{22}$, we have $|\psi(x) - x| \leq \frac{0.006409\, x}{\log x}$. -/)  (latexEnv := "theorem")]theorem theorem_a (x : ℝ) (hx : x ≥ exp 22) :    |ψ x - x| ≤ 0.006409 * x / log x := by  calc |ψ x - x|      ≤ |θ x - x| + (ψ x - θ x) := psi_triangle x    _ ≤ 4.2065e-1 * x / (log x) ^ 3 + (1.001 * sqrt x + 1.78 * x ^ (1 / 3 : ℝ)) := by        linarith [theta_err hx, psi_theta_err <| lt_of_lt_of_le (exp_pos _) hx]    _ ≤ 0.0009 * x / log x + (0.005 * x / log x + 0.0005 * x / log x) := by        linarith [theta_err_simpl hx, sqrt_err hx, cbrt_err hx]    _ ≤ 0.006409 * x / log x := by        have hxlog : 0 ≤ x / log x :=          div_nonneg (le_of_lt (lt_of_lt_of_le (exp_pos _) hx)) (le_of_lt (by linarith [log_ge_22 hx]))        have : 0.0009 * x / log x + (0.005 * x / log x + 0.0005 * x / log x) =               (0.0009 + 0.005 + 0.0005) * (x / log x) := by ring        rw [this, show 0.006409 * x / log x = 0.006409 * (x / log x) from by ring]        apply mul_le_mul_of_nonneg_right _ hxlog        norm_num