CH2.upperRectangleIntegral'_eq_sumResiduesIn

lemma upperRectangleIntegral'_eq_sumResiduesIn (n : ℕ)    (h_rect_mero : MeromorphicOn (fun s ↦ G s * (x : ℂ) ^ s)      (Rectangle ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I)))    (h_no_poles_boundary : Disjoint (RectangleBorder ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I))      {z | meromorphicOrderAt (fun s ↦ G s * (x : ℂ) ^ s) z < 0})    (hfin : {z ∈ l.R \ l.RC | meromorphicOrderAt (fun s ↦ G s * (x : ℂ) ^ s) z < 0}.Finite)    (hsimple : HasSimplePolesOn (fun s ↦ G s * (x : ℂ) ^ s) l.R) :    RectangleIntegral' (fun s ↦ G s * (x : ℂ) ^ s) ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I) =      sumResiduesIn (fun s ↦ G s * (x : ℂ) ^ s) (Rectangle ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I) ∩ {z | meromorphicOrderAt (fun s ↦ G s * (x : ℂ) ^ s) z < 0}) := by  have h_rect_subset_Rpos :      Rectangle ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I) ⊆ l.Rpos :=    l.upperRectangle_subset_Rpos n  have h_rect_subset_R :      Rectangle ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I) ⊆ l.R :=    Set.Subset.trans h_rect_subset_Rpos l.Rpos_subset_R  apply RectangleIntegral'_eq_sumResiduesIn  · simpa using l.hσ n  · simpa using show l.δ ≤ l.T by linarith [l.hδ.2, l.hT]  · exact h_rect_mero  · exact h_no_poles_boundary  · exact Set.Finite.subset hfin (upperRectangle_poles_subset_R_minus_RC l n h_no_poles_boundary)  · exact HasSimplePolesOn.mono hsimple h_rect_subset_R