Complex.summable_logTail

lemma summable_logTail {z : ℂ} (hz : ‖z‖ < 1) (m : ℕ) :    Summable (fun k => z ^ (m + 1 + k) / ((m + 1 + k) : ℂ)) := by  have h_geom : Summable (fun k : ℕ => ‖z‖ ^ k) :=    summable_geometric_of_lt_one (norm_nonneg z) hz  refine Summable.of_norm_bounded (g := fun k => ‖z‖ ^ k) h_geom ?_  intro k  rw [norm_div, norm_pow]  have h1 : (1 : ℝ) ≤ (m + 1 + k : ℝ) := by    have : (0 : ℝ) ≤ (m + k : ℝ) := by positivity    nlinarith  have hnorm : ‖(↑m + 1 + ↑k : ℂ)‖ = (m + 1 + k : ℝ) := by    simpa [Nat.cast_add, Nat.cast_one, add_assoc, add_comm, add_left_comm] using      (Complex.norm_natCast (m + 1 + k))  rw [hnorm]  calc    ‖z‖ ^ (m + 1 + k) / (m + 1 + k : ℝ) ≤ ‖z‖ ^ (m + 1 + k) := by      exact div_le_self (pow_nonneg (norm_nonneg z) _) h1    _ = ‖z‖ ^ (m + 1) * ‖z‖ ^ k := by rw [pow_add]    _ ≤ 1 * ‖z‖ ^ k := by          refine mul_le_mul_of_nonneg_right ?_ (pow_nonneg (norm_nonneg z) k)          exact pow_le_one₀ (norm_nonneg z) (le_of_lt hz)    _ = ‖z‖ ^ k := one_mul _