RS_prime.eq_419

@[blueprint  "rs-419"  (title := "RS equation (4.19) and Mertens' second theorem")  (statement := /--  $$\sum_{p \leq x} \frac{1}{p} = \log \log x + B + \frac{\vartheta(x) - x}{x \log x} $$  $$ - \int_2^x \frac{(\vartheta(y)-y) (1 + \log y)\ dy}{y^2 \log^2 y}.$$-/)  (proof := /-- Follows from Sublemma \ref{rs-413} applied to $f(t) = 1/t$. One can also use this identity to demonstrate convergence of the limit defining $B$.-/)  (latexEnv := "sublemma")  (discussion := 603)]theorem eq_419 {x : ℝ} (hx : 2 ≤ x) :    ∑ p ∈ filter Prime (Iic ⌊x⌋₊), 1 / (p : ℝ) =    log (log x) + meisselMertensConstant + (θ x - x) / (x * log x)    - ∫ y in Set.Ioi x, (θ y - y) * (1 + log y) / (y ^ 2 * log y ^ 2) := by  simp_rw [meisselMertensConstant_identity hx, sub_eq_add_neg _ (∫ y in Set.Ioi x, _),    ← integral_neg, ← div_neg, mul_div_assoc]  have : ∫ (y : ℝ) in Set.Ioi x, (θ y - y) * deriv (fun s ↦ 1 / s / Real.log s) y =    ∫ (a : ℝ) in Set.Ioi x, (θ a - a) * ((1 + Real.log a) / -(a ^ 2 * Real.log a ^ 2)) := by    refine setIntegral_congr_fun measurableSet_Ioi fun y hy => mul_eq_mul_left_iff.2 (Or.inl ?_)    have := deriv_fun_inv'' (y.hasDerivAt_mul_log (by grind)).differentiableAt      (mul_ne_zero_iff.2 ⟨by grind, by linarith [Real.log_pos (by grind : 1 < y)]⟩)    simp_all [deriv_mul_log (by grind : y ≠ 0), div_eq_mul_inv, mul_comm]    ring  congr