Mertens.E₁.summable

@[blueprint  "E1_summable"  (title := "$E_1$ summable")  (statement := /-- The series $E_1 := \sum_p \frac{\log p}{p(p-1)}$ converges. -/)  (proof := /-- We have $\sum_{n=2}^\infty \frac{\log n}{n(n-1)}$ converges by comparison with $\sum_{n=2}^\infty \frac{2\log n}{n^2}$, which converges by the integral test.  By a further application of comparison test we can conclude that $E_1$ converges as well.  Alternatively bound $\log n$ by $2\sqrt n$ and use the existing Mathlib API for $\sum n^{-3/2}$.-/)  (latexEnv := "proposition")  (discussion := 1352)]theorem E₁.summable : Summable (fun p : ℕ ↦ if p.Prime then (log p) / (p*(p-1)) else 0) := by  refine (Real.summable_one_div_nat_rpow.mpr (by norm_num: 1 < (3 : ℝ) / 2)|>.const_div    4).of_nonneg_of_le E₁.summand_nonneg fun n ↦ ?_  split_ifs with h  · grw [Real.log_le_rpow_div (Nat.cast_nonneg _) (by norm_num : 0 < (1 : ℝ) / 2)]    · have denom : (n : ℝ) * ((n : ℝ) - 1) ≥ n ^ 2/ 2 := by        rw [sq, mul_div_assoc]        gcongr        suffices (n : ℝ) ≥ 2 by linarith        exact_mod_cast h.two_le      grw [denom]      · apply le_of_eq        rw [← Real.rpow_natCast]        field_simp        rw [mul_div_assoc, ← Real.rpow_sub (mod_cast h.pos)]        norm_num        rw [Real.rpow_neg (Nat.cast_nonneg _)]        field      · exact div_pos (pow_pos (mod_cast h.pos) _) (by norm_num)    · apply mul_nonneg (Nat.cast_nonneg _)      suffices 1 ≤ (n : ℝ) by linarith      exact_mod_cast h.one_le  · positivity