Mertens.sum_M_eq_summand_le

lemma sum_M_eq_summand_le {N : ℕ} (hN : 0 < N) :    |∑ n ∈ range N, M_eq_summand n - (M - γ)| ≤ 4 / N := by  rw [← tsum_M_eq_summand_eq, ← M_eq_summable.sum_add_tsum_nat_add N]  simp only [sub_add_cancel_left, abs_neg]  rw [← norm_eq_abs]  have summable := summable_nat_add_iff N|>.mpr M_eq_summable.norm  apply norm_tsum_le_tsum_norm summable|>.trans  apply Summable.tsum_le_tsum (fun _ ↦ M_eq_summand_bound _) summable _|>.trans  · conv => lhs; arg 1; ext; rw [← mul_one_div]    rw [tsum_mul_left]    push_cast    grw [sum_one_div_sq_le (mod_cast hN)]    ring_nf    rfl  · exact (summable_nat_add_iff N|>.mpr (summable_one_div_nat_pow.mpr one_lt_two))|>.const_div _