RS_prime.mertens_first_theorem

@[blueprint  "rs-420"]theorem mertens_first_theorem : Filter.atTop.Tendsto (fun x : ℝ ↦    ∑ p ∈ filter Nat.Prime (Iic ⌊x⌋₊), Real.log p / p - log x) (𝓝 mertensConstant) := by  have lem : ∀ᶠ x in atTop, mertensConstant + (θ x - x) / x    + ∫ y in Set.Ioi x, - ((θ y - y) / (y ^ 2)) =    ∑ p ∈ filter Nat.Prime (Iic ⌊x⌋₊), Real.log p / p - log x := by    filter_upwards [Ici_mem_atTop 2] with y hy    rw [eq_420 hy, integral_neg]    ring  rw [← add_zero mertensConstant, ← add_zero (_ + _)]  refine ((tendsto_const_nhds.add ?_).add    (ioiIntegral_tendsto_zero 2 integrableOn_deriv_inv.1 tendsto_id)).congr' lem  · obtain ⟨C, hC⟩ := pnt    refine squeeze_zero_norm' (a := fun x => C / Real.log x ^ 2) ?_ ?_    · filter_upwards [Ici_mem_atTop 2] with y hy      simp only [norm_div, norm_of_nonneg (by grind : 0 ≤ y), norm_eq_abs]      grw [hC.2 y hy]      · rw [div_right_comm, mul_div_cancel_right₀ _ (by grind)]      · grind    · exact ((tendsto_pow_atTop (by linarith : 2 ≠ 0)).comp tendsto_log_atTop).const_div_atTop C