CH2.lemma_5_1_g

@[blueprint  "ch2-lemma-5-1-g"  (title := "Residue-sum exhaustion (CH2 Lemma 5.1, residue limit)")  (statement := /--  If $f$ is meromorphic on a region $S$ and has only finitely many poles there, then the truncated  residue sums over $S \cap \{\Re s > \sigma_n\}$ converge, as $n \to \infty$, to the full sum  over $S$. (Indeed they are eventually equal to it, once $\sigma_n$ has dropped below the real  part of every pole.) -/)  (proof := /-- Since $\sigma_n \to -\infty$ and there are finitely many poles in $S$, for all  large $n$ the set $\{\Re s > \sigma_n\}$ contains every pole of $f$ in $S$; meromorphicity on  $S$ makes the residue vanish at non-poles, so the truncated sum is then constant and equals the  full residue sum over $S$. -/)  (latexEnv := "sublemma")  (discussion := 1454)]theorem lemma_5_1_g (f : ℂ → ℂ) (S : Set ℂ)    (hmero : MeromorphicOn f S)    (hfin : {z ∈ S | meromorphicOrderAt f z < 0}.Finite) :    Filter.Tendsto (fun n ↦ sumResiduesIn f (S ∩ {z | l.σ n < z.re})) Filter.atTop      (nhds (sumResiduesIn f S)) := by  let P : Set ℂ := {z | meromorphicOrderAt f z < 0}  have hP_fin : (S ∩ P).Finite := by    simpa [P, Set.setOf_and] using hfin  obtain ⟨B, hB⟩ : ∃ B : ℝ, ∀ z ∈ S ∩ P, B ≤ z.re := by    obtain ⟨B, hB⟩ := (hP_fin.image Complex.re).exists_ge    exact ⟨B, fun z hz ↦ hB z.re ⟨z, hz, rfl⟩⟩  have h_residue_zero : ∀ s ∈ S, s ∉ P → residue f s = 0 := fun s hsS hs_not_pole ↦    residue_eq_zero_of_not_pole_of_meromorphicAt (hmero s hsS)      (le_of_not_gt (fun h ↦ hs_not_pole h))  have h_eventually_eq : ∀ᶠ n in Filter.atTop, sumResiduesIn f (S ∩ {z | l.σ n < z.re}) = sumResiduesIn f S := by    filter_upwards [l.hlim.eventually_lt_atBot B] with n hn    have h_set_eq : (S ∩ {z | l.σ n < z.re}) ∩ P = S ∩ P :=      Set.Subset.antisymm (fun z hz ↦ ⟨hz.1.1, hz.2⟩) (fun z hz ↦ ⟨⟨hz.1, lt_of_lt_of_le hn (hB z hz)⟩, hz.2⟩)    have h_trunc_eq : sumResiduesIn f ((S ∩ {z | l.σ n < z.re}) ∩ P) = sumResiduesIn f (S ∩ {z | l.σ n < z.re}) :=      sumResiduesIn_inter_eq_of_set_eq (F := f) (Rn := S ∩ {z | l.σ n < z.re}) (S2 := S ∩ {z | l.σ n < z.re}) (P := P)        rfl (fun s hs_trunc hs_not_pole ↦ h_residue_zero s hs_trunc.1 hs_not_pole)    calc      sumResiduesIn f (S ∩ {z | l.σ n < z.re}) = sumResiduesIn f ((S ∩ {z | l.σ n < z.re}) ∩ P) := h_trunc_eq.symm      _ = sumResiduesIn f (S ∩ P) := by rw [h_set_eq]      _ = sumResiduesIn f S := sumResiduesIn_inter_eq_of_set_eq (F := f) (Rn := S) (S2 := S) (P := P) rfl h_residue_zero  exact tendsto_nhds_of_eventually_eq h_eventually_eq