RS_prime.eq_420

@[blueprint  "rs-420"  (title := "RS equation (4.19) and Mertens' first theorem")  (statement := /--  $$\sum_{p \leq x} \frac{\log p}{p} = \log x + E + \frac{\vartheta(x) - x}{x} $$  $$ - \int_2^x \frac{(\vartheta(y)-y)\ dy}{y^2}.$$-/)  (proof := /-- Follows from Sublemma \ref{rs-413} applied to $f(t) = \log t / t$.  Convergence will need Theorem \ref{rs-pnt}. -/)  (latexEnv := "sublemma")  (discussion := 604)]theorem eq_420 {x : ℝ} (hx : 2 ≤ x) :    ∑ p ∈ filter Prime (Iic ⌊x⌋₊), Real.log p / p =    log x + mertensConstant + (θ x - x) / x - ∫ y in Set.Ioi x, (θ y - y) / (y ^ 2) := by  have diff_log_inv_id : ∀ t ∈ Set.Ici 2, DifferentiableAt ℝ (fun x => Real.log x / x) t := by    fun_prop (disch := grind)  have ioiIntegral_eq : ∫ (y : ℝ) in Set.Ioi x, (θ y - y) * deriv (fun s ↦    Real.log s / s / Real.log s) y = ∫ (y : ℝ) in Set.Ioi x, - ((θ y - y) / y ^ 2) := by    refine setIntegral_congr_fun measurableSet_Ioi fun y hy => ?_    simp [field, deriv_eq (by grind : 2 ≤ y)]  have integral_eq_log : ∫ y in 2..x, 1 / y = log x - Real.log 2 := by    have {y} (hy : y ∈ Set.uIcc 2 x) := (Set.uIcc_of_le hx ▸ hy).1    refine intervalIntegral.integral_eq_sub_of_hasDerivAt (f := Real.log) (fun y hy => ?_) ?_    · simpa using hasDerivAt_log (by grind)    · exact ContinuousOn.intervalIntegrable_of_Icc hx (by fun_prop (disch := grind))  rw [eq_415 diff_log_inv_id hx, mertensConstant, mul_div_right_comm, log_div_log_eq (by grind),    ioiIntegral_eq, intervalIntegral_eq hx, integral_eq_log, integral_neg]  · ring  · refine integrableOn_deriv_inv.1.congr_fun (fun y hy => ?_) measurableSet_Ioi    simp [field, deriv_eq (by grind : 2 ≤ y)]  · exact (integrableOn_deriv_inv.2 x hx).congr fun y hy =>      (deriv_eq (Set.uIoc_of_le hx ▸ hy).1.le).symm