Complex.norm_logTail_le

lemma norm_logTail_le {z : ℂ} (hz : ‖z‖ < 1) (m : ℕ) :    ‖logTail m z‖ ≤ ‖z‖ ^ (m + 1) / (1 - ‖z‖) := by  dsimp only [logTail]  have h_rhs_summable : Summable (fun k => ‖z‖ ^ (m + 1 + k)) := by    simpa [pow_add] using      (summable_geometric_of_lt_one (norm_nonneg z) hz).mul_left (‖z‖ ^ (m + 1))  have h_norm_summable : Summable (fun k => ‖z ^ (m + 1 + k) / ((m + 1 + k) : ℂ)‖) := by    refine Summable.of_nonneg_of_le (fun _ => norm_nonneg _) ?_ h_rhs_summable    intro k    rw [norm_div, norm_pow]    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]    have hm : 1 ≤ (m + 1 + k : ℝ) := by      have : (0 : ℝ) ≤ (m + k : ℝ) := by positivity      nlinarith    exact div_le_self (pow_nonneg (norm_nonneg z) _) hm  calc    ‖∑' k, z ^ (m + 1 + k) / ((m + 1 + k) : ℂ)‖        ≤ ∑' k, ‖z ^ (m + 1 + k) / ((m + 1 + k) : ℂ)‖ :=          norm_tsum_le_tsum_norm h_norm_summable    _ ≤ ∑' k, ‖z‖ ^ (m + 1 + k) := by          refine h_norm_summable.tsum_le_tsum ?_ h_rhs_summable          intro k          rw [norm_div, norm_pow]          have hm : 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]          exact div_le_self (pow_nonneg (norm_nonneg z) _) hm    _ = ‖z‖ ^ (m + 1) / (1 - ‖z‖) := by          have h_eq :              (fun k => ‖z‖ ^ (m + 1 + k)) = fun k => ‖z‖ ^ (m + 1) * ‖z‖ ^ k := by            ext k            rw [pow_add]          rw [h_eq, tsum_mul_left]          have h_geom := hasSum_geometric_of_lt_one (norm_nonneg z) hz          rw [h_geom.tsum_eq, div_eq_mul_inv]