RS_prime.mertens_second_theorem'

@[blueprint  "rs-419"]theorem mertens_second_theorem' :    ∃ C, ∀ x ≥ 2, |∑ p ∈ filter Prime (Iic ⌊x⌋₊), 1 / (p : ℝ) - log (log x)| ≤ C := by  obtain ⟨C, hC⟩ := pnt  refine ⟨|meisselMertensConstant| + C / Real.log 2 ^ 3 +    ∫ y in Set.Ioi 2, |(θ y - y) * deriv (fun t ↦ 1 / t / Real.log t) y|, fun x hx => ?_⟩  calc  _ ≤ |meisselMertensConstant + (θ x - x) / (x * log x)    + ∫ y in Set.Ioi x, (θ y - y) * deriv (fun t ↦ 1 / t / Real.log t) y| := by    rw [meisselMertensConstant_identity hx]; ring_nf; rfl  _ ≤ |meisselMertensConstant| + |(θ x - x) / (x * log x)|    + ∫ y in Set.Ioi x, |(θ y - y) * deriv (fun t ↦ 1 / t / Real.log t) y| := by    grw [sub_eq_add_neg, abs_add_le, abs_add_le, abs_integral_le_integral_abs]  _ ≤ _ := by    gcongr    · grw [abs_div, hC.2 x hx, abs_of_nonneg (mul_nonneg (by grind) (log_nonneg (by grind))),        div_right_comm, ← div_div, mul_div_cancel_right₀ _ (by grind)]      ring_nf      gcongr      · exact hC.1      · exact inv_nonneg.2 (log_nonneg (by grind))    · filter_upwards with a      apply abs_nonneg    · exact integrableOn_deriv_inv_div_log.1.abs