Complex.continuousOn_digamma_of_re_ge_norm_le

theorem continuousOn_digamma_of_re_ge_norm_le {a R : ℝ} (ha : 0 < a) (ha1 : a ≤ 1) :    ContinuousOn digamma ({z : ℂ | a ≤ z.re} ∩ {z : ℂ | ‖z‖ ≤ R}) := by  set s : Set ℂ := {z : ℂ | a ≤ z.re} ∩ {z : ℂ | ‖z‖ ≤ R}  have hu : Summable (fun m : ℕ => (R + 1) / (a * ((m : ℝ) + 1) ^ 2)) := by    refine (summable_one_div_natCast_add_one_sq.mul_left ((R + 1) / a)).congr fun m => ?_    rw [mul_one_div, div_div]  have hseries : ContinuousOn      (fun z : ℂ => ∑' m : ℕ, (1 / ((m : ℂ) + 1) - 1 / ((m : ℂ) + z))) s := by    refine continuousOn_tsum      (f := fun m (z : ℂ) => 1 / ((m : ℂ) + 1) - 1 / ((m : ℂ) + z))      (u := fun m : ℕ => (R + 1) / (a * ((m : ℝ) + 1) ^ 2)) ?hf hu ?hbound    · intro m      have hden : ContinuousOn (fun z : ℂ => ((m : ℂ) + z)⁻¹) s := by        refine (continuousOn_const.add continuousOn_id).inv₀ ?_        intro z hz hzero        change (m : ℂ) + z = 0 at hzero        have hza : a ≤ z.re := hz.1        have hzpos : 0 < (((m : ℂ) + z) : ℂ).re := by          rw [add_re, natCast_re]          have hm_nonneg : 0 ≤ (m : ℝ) := by positivity          linarith [ha, hza, hm_nonneg]        rw [hzero] at hzpos        norm_num at hzpos      simpa only [one_div] using continuousOn_const.fun_sub hden    · intro m z hz      have h := norm_inv_add_one_sub_inv_le ha ha1 hz.1 hz.2 m      simpa [one_div, add_comm] using h  exact (continuousOn_const.add hseries).congr fun z hz => by    exact digamma_eq_tsum fun n hzn => by      have hre := congrArg Complex.re hzn      have hza : a ≤ z.re := hz.1      have hzpos : 0 < z.re := lt_of_lt_of_le ha hz.1      have hre' : z.re = -(n : ℝ) := by        simpa using hre      have hn : 0 ≤ (n : ℝ) := by positivity      linarith