Mertens.E₂Λ.abs_le

@[blueprint  "Mertens-second-error-mangoldt-bound"  (title := "Bound for second Mertens error (von Mangoldt form)")  (statement := /-- For any $x \geq 2$, one has$$ |E_{2,\Lambda}(x)| \leq \frac{\log 4 + 6}{\log x}.$$-/)  (proof := /--  Insert Lemma \ref{Mertens-first-error-mangoldt-le} and Lemma \ref{Mertens-first-error-mangoldt-ge} into Lemma \ref{Mertens-second-error-mangoldt-eq} and use the triangle inequality to obtain the required upper and lower bounds.  -/)  (latexEnv := "corollary")  (discussion := 1318)]theorem E₂Λ.abs_le {x : ℝ} (hx : 2 ≤ x) :    |E₂Λ x| ≤ (log 4 + 6) / log x := by    have : 0 < log x := by apply log_pos; linarith    rw [E₂Λ.eq hx, abs_le']    constructor    · grw [E₁Λ.le (by linarith)]      have : ∫ t in Set.Ioi x, E₁Λ t / (t * log t^2) ≥ - 2 / log x := calc        _ ≥ ∫ t in Set.Ioi x, (-2) / (t * log t^2) := by          apply MeasureTheory.setIntegral_mono_on (integrable_const_div_mul_log_sq (-2) hx)            (integrable_E₁Λ_div_mul_log_sq hx) (by measurability)          intro y hy; simp at hy          have : 1 < y := by linarith          have : 0 < log y := log_pos this          gcongr; exact E₁Λ.ge (by linarith)        _ = _ := integ_div_mul_log_sq (-2) hx      grw [this]      grind    grw [E₁Λ.ge (by linarith)]    have : ∫ t in Set.Ioi x, E₁Λ t / (t * log t^2) ≤ (log 4 + 4) / log x := calc        _ ≤ ∫ t in Set.Ioi x, (log 4 + 4) / (t * log t^2) := by          apply MeasureTheory.setIntegral_mono_on (integrable_E₁Λ_div_mul_log_sq hx)            (integrable_const_div_mul_log_sq (log 4 + 4) hx) (by measurability)          intro y hy; simp at hy          have : 1 < y := by linarith          have : 0 < log y := log_pos this          gcongr; exact E₁Λ.le (by linarith)        _ = _ := integ_div_mul_log_sq (log 4 + 4) hx    grw [this]    grind