Mertens.sum_prime_div_eq_log_log

@[blueprint  "Mertens-second-theorem-prime-weak"  (title := "Mertens' second theorem (weak prime form)")  (statement := /-- For any $x \geq 2$, one has$$ \sum_{p \leq x} \frac{1}{p} = \log \log x + O(1). $$-/)  (proof := /-- Immediate from previous two corollaries.  -/)  (discussion := 1327)]theorem sum_prime_div_eq_log_log : ∃ C, ∀ x, 2 ≤ x →    |∑ p ∈ Ioc 0 ⌊x⌋₊ with p.Prime, (1:ℝ) / p - log (log x)| ≤ C := by    use |M| + (log 4 + 6 + E₁) / log 2    intro x hx    rw [sum_prime_div_eq]    calc      _ = |M + E₂p x| := by ring_nf      _ ≤ |M| + (log 4 + 6 + E₁) / log x := by grw [abs_add_le, E₂p.abs_le hx]      _ ≤ _ := by        gcongr        have : 0 < log 4 := by apply log_pos; norm_num        linarith [E₁.nonneg]