ZetaAppendix.lemma_abadeulmit2_tsum_one_div_sub_int_sq

lemma lemma_abadeulmit2_tsum_one_div_sub_int_sq {z : ℂ} (hz : z ∈ integerComplement) :  ∑' (n : ℤ), 1 / (z - n) ^ 2 =  deriv (fun w ↦ -π * Complex.cot (π * w)) z := by  set f := fun w : ℂ ↦ -π * Complex.cot (π * w)  set S := fun w : ℂ ↦ ∑' (n : ℤ), 1 / (w - n) ^ 2  suffices HasDerivAt f (∑' (n : ℤ), 1 / (z - n) ^ 2) z from this.deriv.symm  apply HasDerivAt.congr_of_eventuallyEq (f := fun w ↦ f z + (w - z) * ∫ t in (0:ℝ)..1, S (z + t * (w - z)))  · apply HasDerivAt.const_add    rw [hasDerivAt_iff_isLittleO]    simp only [sub_self, mul_zero, add_zero]    set g := fun x' ↦ ∫ (t : ℝ) in 0..1, S (z + ↑t * (x' - z))    simp only [zero_mul, sub_zero, smul_eq_mul, ← mul_sub]    apply Asymptotics.isLittleO_of_tendsto    · intro x' hx; simp [sub_eq_zero.mp hx]    · have h_eq : (fun x ↦ (x - z) * ((∫ (t : ℝ) in 0..1, S (z + ↑t * (x - z))) - ∑' (n : ℤ), 1 / (z - ↑n) ^ 2) / (x - z)) =            (fun x ↦ (∫ (t : ℝ) in 0..1, S (z + ↑t * (x - z))) - ∑' (n : ℤ), 1 / (z - ↑n) ^ 2) := by        ext x        rcases eq_or_ne x z with rfl | hx        · simp [S]        · rw [mul_div_cancel_left₀ _ (sub_ne_zero.mpr hx)]      rw [h_eq, tendsto_sub_nhds_zero_iff]      have hgz : g z = ∑' (n : ℤ), 1 / (z - ↑n) ^ 2 := by        simp only [g, sub_self, mul_zero, add_zero]        rw [intervalIntegral.integral_const, sub_zero, Complex.real_smul, Complex.ofReal_one, one_mul]      rw [← hgz]      apply (lemma_abadeulmit2_continuousAt_integral_tsum_one_div_sub_int_sq hz).tendsto  · obtain ⟨ε, hε, h_ball⟩ := Metric.isOpen_iff.1 (Complex.isOpen_compl_range_intCast) z hz    filter_upwards [Metric.ball_mem_nhds z hε] with w hw    rw [lemma_abadeulmit2_integral_eq_cot_diff (h_ball hw) hz]    · dsimp [f]; ring    · intro t ht      apply h_ball      apply (convex_ball z ε).segment_subset (Metric.mem_ball_self hε) hw      rw [segment_eq_image]      refine ⟨t, ht, ?_⟩      simp; ring