Mertens.E₃.abs_le

@[blueprint  "Mertens-third-theorem-error-le"  (title := "Mertens' third theorem error bound")  (statement := /-- For any $x \geq 2$, one has$$ E_3(x) = O\left(\frac{1}{\log x}\right) $$-/)  (proof := /--Estimating the error in \ref{Meissel-Mertens-eq} using the first order Taylor expansion of log one gets$$\sum_{p \le x}(\log (1-1/p)+1/p) = (M - \gamma) + O(1/x).$$The result follows by combining with \ref{Mertens-second-error-prime-abs-le}.  -/)  (discussion := 1330)]theorem E₃.abs_le : ∃ C, ∀ x, 2 ≤ x → |E₃ x| ≤ C / log x := by  unfold E₃  refine ⟨4 + (log 4 + 6 + E₁), fun x hx ↦ ?_⟩  calc  _ = |(∑ n ∈ Ioc 0 ⌊x⌋₊, M_eq_summand n - (M - γ)) - E₂p x| := by    unfold E₂p    have (n : ℕ) : M_eq_summand n = (if n.Prime then log (1 - 1 / n) else 0) + (if n.Prime then (1 : ℝ) / n else 0) := by      unfold M_eq_summand      split_ifs      · rfl      · ring    simp_rw [this]    rw [sum_filter, sum_filter, sum_add_distrib, γ.eq_eulerMascheroni]    ring_nf  _ ≤ _ := by    grw [abs_sub, E₂p.abs_le hx, sum_M_eq_summand_le' hx]    have : 4 / x ≤ 4 / log x := by      gcongr      · exact log_pos (by linarith)      · exact log_le_self (by linarith)    grw [this]    rw [← add_div]