Mertens.sum_one_div_sq_le

lemma sum_one_div_sq_le {N : ℝ} (hN : 1 ≤ N) :    ∑' (n : ℕ), (1 : ℝ) / (n + N) ^ 2 ≤ 2 / N := by  grw [AntitoneOn.tsum_le_integral (f := (fun t ↦ 1 / (t + N) ^ 2))]  · have hd : ∀ x ∈ Set.Ici 0, HasDerivAt (fun t ↦ -1 / (t + N)) (1 / (x + N) ^ 2) x := by      intro t ht      convert! HasDerivAt.fun_div (d' := (1 : ℝ)) (hasDerivAt_const ..) _ _ using 1      · ring      · simpa using hasDerivAt_id' t      · simp at ht        linarith    have lim : Tendsto (fun t ↦ -1 / (t + N)) atTop (nhds 0) := by      exact (tendsto_atTop_add_const_right atTop N tendsto_id).const_div_atTop _    rw [MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg' hd (fun _ _ ↦ (by positivity)) lim]    ring_nf    rw [mul_two]    gcongr    field_simp    exact hN  · unfold AntitoneOn    intro a ha b hb h    beta_reduce    simp at ha hb    gcongr  · convert! integrableOn_add_rpow_Ioi_of_lt (by norm_num : (-2 : ℝ) < -1) (by linarith : -N < 0) using 2    simp    rfl  · exact fun _ _ ↦ (by positivity)