Complex.hasSum_digamma

theorem hasSum_digamma {z : ℂ} (hz : ∀ n : ℕ, z ≠ -n) :    HasSum (fun n : ℕ => 1 / ((n : ℂ) + 1) - 1 / ((n : ℂ) + z))      (digamma z + Real.eulerMascheroniConstant) := by  suffices h : HasSum (fun m : ℕ => ((m : ℂ) + 1)⁻¹ - (z + m)⁻¹)      (digamma z + Real.eulerMascheroniConstant) by    have e : (fun n : ℕ => 1 / ((n : ℂ) + 1) - 1 / ((n : ℂ) + z))        = fun m : ℕ => ((m : ℂ) + 1)⁻¹ - (z + m)⁻¹ := by      funext m      rw [one_div, one_div, add_comm (m : ℂ) z]    rw [e]    exact h  obtain ⟨N, hN⟩ : ∃ N : ℕ, -(N : ℝ) < z.re :=    ⟨⌈-z.re⌉₊ + 1, by have := Nat.le_ceil (-z.re); push_cast; linarith⟩  induction N generalizing z with  | zero =>    apply hasSum_digamma_of_re_pos    simpa using hN  | succ N ih =>    by_cases hcase : -(N : ℝ) < z.re    · exact ih hz hcase    · -- shift by one and use the recurrence      have hz1 : ∀ n : ℕ, z + 1 ≠ -(n : ℂ) := by        intro n hcon        apply hz (n + 1)        push_cast        linear_combination hcon      have hre1 : -(N : ℝ) < (z + 1).re := by        rw [add_re, one_re]        push_cast at hN        linarith      have hih := ih hz1 hre1      rw [digamma_apply_add_one z hz] at hih      have hzm : ∀ n : ℕ, z + (n : ℂ) ≠ 0 := fun n hcon => hz n (by linear_combination hcon)      have hnorm_lb : ∀ n : ℕ, (n : ℝ) - ‖z‖ ≤ ‖z + n‖ := by        intro n        have h := norm_sub_norm_le (n : ℂ) (-z)        rw [sub_neg_eq_add, norm_neg, norm_natCast] at h        rw [show z + (n : ℂ) = (n : ℂ) + z from add_comm _ _]        exact h      have ha0 : Tendsto (fun n : ℕ => (z + (n : ℂ))⁻¹) atTop (𝓝 0) := by        rw [tendsto_zero_iff_norm_tendsto_zero]        simp only [norm_inv]        apply Filter.Tendsto.inv_tendsto_atTop        apply tendsto_atTop_mono hnorm_lb        have h := tendsto_atTop_add_const_right atTop (-‖z‖) tendsto_natCast_atTop_atTop        exact h.congr fun n => by ring      have hts : Summable (fun n : ℕ => (z + (n : ℂ))⁻¹ - (z + ((n + 1 : ℕ) : ℂ))⁻¹) := by        apply Summable.of_norm_bounded_eventually_nat          (g := fun n : ℕ => 4 * (1 / ((n : ℝ) + 1) ^ 2))          (summable_one_div_natCast_add_one_sq.mul_left _)        filter_upwards [eventually_ge_atTop ⌈2 * ‖z‖ + 1⌉₊] with n hn        have hnR : 2 * ‖z‖ + 1 ≤ (n : ℝ) := le_trans (Nat.le_ceil _) (by exact_mod_cast hn)        have hz0 : (0 : ℝ) ≤ ‖z‖ := norm_nonneg z        have hb1 : ((n : ℝ) + 1) / 2 ≤ ‖z + n‖ := le_trans (by linarith) (hnorm_lb n)        have hb2 : ((n : ℝ) + 1) / 2 ≤ ‖z + ((n + 1 : ℕ) : ℂ)‖ := by          refine le_trans ?_ (hnorm_lb (n + 1))          push_cast          linarith        have hid : (z + (n : ℂ))⁻¹ - (z + ((n + 1 : ℕ) : ℂ))⁻¹            = ((z + n) * (z + ((n + 1 : ℕ) : ℂ)))⁻¹ := by          have h1 := hzm n          have h2 := hzm (n + 1)          field_simp          push_cast          ring        rw [hid, norm_inv, norm_mul,          show (4 : ℝ) * (1 / ((n : ℝ) + 1) ^ 2)            = ((((n : ℝ) + 1) / 2) * (((n : ℝ) + 1) / 2))⁻¹ by field_simp; ring]        gcongr      have htel := hasSum_sub_succ_of_tendsto_zero ha0 hts      simp only [Nat.cast_zero, add_zero] at htel      have hfin := hih.sub htel      have e2 : (fun n : ℕ => (((n : ℂ) + 1)⁻¹ - (z + 1 + n)⁻¹)            - ((z + (n : ℂ))⁻¹ - (z + ((n + 1 : ℕ) : ℂ))⁻¹))          = fun n : ℕ => ((n : ℂ) + 1)⁻¹ - (z + n)⁻¹ := by        funext n        push_cast        ring      rw [e2] at hfin      convert! hfin using 1      ring