RS_prime.mertens_second_theorem

@[blueprint  "rs-419"]theorem mertens_second_theorem : Filter.atTop.Tendsto (fun x : ℝ ↦    ∑ p ∈ filter Nat.Prime (Iic ⌊x⌋₊), 1 / (p : ℝ) - log (log x)) (𝓝 meisselMertensConstant) := by  have lem : ∀ᶠ x in atTop, meisselMertensConstant + ((θ x - x) / (x * log x) +    ∫ y in Set.Ioi x, (θ y - y) * deriv (fun s ↦ 1 / s / Real.log s) y) =    ∑ p ∈ filter Nat.Prime (Iic ⌊x⌋₊), 1 / (p : ℝ) - log (log x):= by    filter_upwards [Ici_mem_atTop 2] with y hy    rw [meisselMertensConstant_identity hy]    ring  rw [← add_zero meisselMertensConstant, ← add_zero 0]  refine (tendsto_const_nhds.add (Tendsto.add ?_    (ioiIntegral_tendsto_zero 2 integrableOn_deriv_inv_div_log.1 tendsto_id))).congr' lem  · obtain ⟨C, hC⟩ := pnt    refine squeeze_zero_norm' (a := fun x => C / Real.log x ^ 3) ?_ ?_    · filter_upwards [Ici_mem_atTop 2] with y hy      have h1 {y : ℝ} (hy : y ∈ Set.Ici 2) : 0 < y := by grind      have h2 {y : ℝ} (hy : y ∈ Set.Ici 2) : 0 ≤ log y := log_nonneg (by grind)      simp only [norm_div, norm_mul, norm_of_nonneg (h1 hy).le, norm_eq_abs, norm_of_nonneg (h2 hy)]      grw [hC.2 y hy]      · rw [div_right_comm, ← div_div, mul_div_cancel_right₀ _ (by grind)]; field_simp; rfl      · exact mul_nonneg (h1 hy).le (h2 hy)    · exact ((tendsto_pow_atTop (by linarith : 3 ≠ 0)).comp tendsto_log_atTop).const_div_atTop C