RS_prime.eq_418

@[blueprint  "rs-418"  (title := "RS equation (4.18)")  (statement := /--  $$\sum_{p \leq x} \frac{1}{p} = \frac{\vartheta(x)}{x \log x} + \int_2^x \frac{\vartheta(y) (1 + \log y)\ dy}{y^2 \log^2 y}.$$-/)  (proof := /-- Follows from Sublemma \ref{rs-413} applied to $f(t) = 1/t$. -/)  (latexEnv := "sublemma")  (discussion := 652)]theorem eq_418 {x : ℝ} (hx : 2 ≤ x) :    ∑ p ∈ filter Prime (Iic ⌊x⌋₊), 1 / (p : ℝ) = θ x / (x * log x) +    ∫ y in 2..x, θ y * (1 + log y) / (y ^ 2 * log y ^ 2) := by  have : ∀ t ∈ Set.Icc 2 x, DifferentiableAt ℝ (fun y : ℝ ↦ 1 / y) t :=    fun y hy => (by fun_prop (disch := grind))  have integrable : IntervalIntegrable (fun t ↦ deriv (fun y ↦ 1 / y / Real.log y) t) volume 2 x := by    apply IntervalIntegrable.congr (f := (fun y ↦ -(1 + Real.log y) / (y ^ 2 * Real.log y ^ 2)))    · intro y hy      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 only [div_div, fun t : ℝ => one_div (t * log t), this,        deriv_mul_log (by grind : y ≠ 0)]      ring    · refine  ContinuousOn.intervalIntegrable fun t ht ↦ ContinuousAt.continuousWithinAt ?_      rw [Set.uIcc_of_le hx] at ht      apply ContinuousAt.div (by fun_prop (disch := grind)) (by fun_prop (disch := grind))      simp; grind  rw [eq_413 (f := fun x => 1 / x) hx this integrable, mul_comm_div, one_mul, div_div, sub_eq_add_neg,    ← intervalIntegral.integral_neg, add_left_cancel_iff]  refine intervalIntegral.integral_congr fun y hy => ?_  have hy := Set.uIcc_of_le hx ▸ hy  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 only [neg_mul_eq_mul_neg, mul_div_assoc, mul_left_cancel_iff_of_pos    (theta_pos hy.1), div_div, fun t : ℝ => one_div (t * log t), this,    deriv_mul_log (by grind : y ≠ 0)]  ring