CH2.upperRectangle_no_poles_boundary

lemma upperRectangle_no_poles_boundary (l : LadderParams) (n : ℕ)    (hG : ∀ s, G s = G_circ s + (Real.sign s.im : ℂ) * G_star s)    (hG_circ_mero : MeromorphicOn G_circ l.R) (hG_star_mero : MeromorphicOn G_star l.R)    (hx₀ : 1 ≤ x₀)    (hG_bdd : IsBoundedNoPolesOn (fun s ↦ G s * (x₀ : ℂ) ^ s) l.Rboundary)    (hGc_L : IsBoundedNoPolesOn (fun s ↦ G_circ s * (x₀ : ℂ) ^ s) l.L)    (hGc_contour : IsBoundedNoPolesOn (fun s ↦ G_circ s * (x₀ : ℂ) ^ s) l.admissible_contour)    (hGs_L : IsBoundedNoPolesOn (fun s ↦ G_star s * (x₀ : ℂ) ^ s) l.L)    (hGs_contour : IsBoundedNoPolesOn (fun s ↦ G_star s * (x₀ : ℂ) ^ s) l.admissible_contour)    (hx : x₀ < x) :    Disjoint (RectangleBorder ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I))      {z | meromorphicOrderAt (fun s ↦ G s * (x : ℂ) ^ s) z < 0} := by  rw [Set.disjoint_left]  rintro z hz hz_pole  simp only [Set.mem_setOf_eq] at hz_pole  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  have hz_rect : z ∈ Rectangle ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I) :=    rectangleBorder_subset_rectangle _ _ hz  have h_im_bounds : z.im ∈ Set.Icc l.δ l.T := by    have h_mem := (mem_Rect (by simpa using l.hσ n) (by simpa using show l.δ ≤ l.T by linarith [l.hδ.2, l.hT]) z).mp hz_rect    exact ⟨by simpa using h_mem.2.2.1, by simpa using h_mem.2.2.2⟩  have hz_im_pos : 0 < z.im := lt_of_lt_of_le l.hδ.1 h_im_bounds.1  have h_sign : (Real.sign z.im : ℂ) = 1 := by simp [Real.sign_of_pos hz_im_pos]  have abs_zim_le : |z.im| ≤ l.T := by    rw [abs_of_pos hz_im_pos]    exact h_im_bounds.2  have hG_eq : G =ᶠ[nhds z] G_circ + G_star := by    have hpos_mem : {t : ℂ | 0 < t.im} ∈ nhds z :=      (isOpen_lt continuous_const Complex.continuous_im).mem_nhds hz_im_pos    filter_upwards [hpos_mem] with t ht    have hsign : (Real.sign t.im : ℂ) = 1 := by simp [Real.sign_of_pos ht]    simp [hG t, hsign]  have hz_R : z ∈ l.R := h_rect_subset_R hz_rect  have hGc_mero : MeromorphicAt G_circ z := hG_circ_mero z hz_R  have hGs_mero : MeromorphicAt G_star z := hG_star_mero z hz_R  have hG_mero : MeromorphicAt G z :=    (hGc_mero.add hGs_mero).congr (Filter.EventuallyEq.filter_mono hG_eq.symm nhdsWithin_le_nhds)  have hx_pos : 0 < x := by linarith  have hpow_mero : MeromorphicAt (fun s ↦ (x : ℂ) ^ s) z := meromorphicAt_rpow hx_pos z  have hpow_order : meromorphicOrderAt (fun s ↦ (x : ℂ) ^ s) z = 0 := meromorphicOrderAt_rpow hx_pos z  have extract_order : ∀ (F : ℂ → ℂ) (S : Set ℂ) (hF_mero : MeromorphicAt F z),      IsBoundedNoPolesOn (fun s ↦ F s * (x₀ : ℂ) ^ s) S → z ∈ S → 0 ≤ meromorphicOrderAt F z :=    fun F S hF_mero h_bdd hz_S ↦ meromorphicOrderAt_nonneg_of_bounded hx₀ hF_mero h_bdd hz_S  have combine_orders : 0 ≤ meromorphicOrderAt G_circ z → 0 ≤ meromorphicOrderAt G_star z → 0 ≤ meromorphicOrderAt G z :=    meromorphicOrderAt_add_nonneg hGc_mero hGs_mero hG_eq  have h_nonneg_G : 0 ≤ meromorphicOrderAt G z := by    have h_sigma_le : l.σ n ≤ 1 := l.hσ n    have h_delta_le : l.δ ≤ l.T := by linarith [l.hδ.1, l.hδ.2, l.hT]    simp only [RectangleBorder, Set.mem_union, Complex.mem_reProdIm, Set.mem_singleton_iff,      Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im,      mul_zero, add_zero, sub_zero, mul_one, zero_add,      Complex.add_im, Complex.ofReal_im, Complex.mul_im, Complex.one_re, Complex.one_im,      Set.uIcc_of_le h_sigma_le, Set.uIcc_of_le h_delta_le] at hz    rcases hz with (((⟨hz_re, hz_im⟩ | ⟨hz_re, hz_im⟩) | ⟨hz_re, hz_im⟩) | ⟨hz_re, hz_im⟩)    · have hz_contour : z ∈ l.admissible_contour := by        left        exact ⟨hz_re.2, hz_im⟩      exact combine_orders (extract_order G_circ l.admissible_contour hGc_mero hGc_contour hz_contour)                           (extract_order G_star l.admissible_contour hGs_mero hGs_contour hz_contour)    · cases n with      | zero =>        have hz_Rb : z ∈ l.Rboundary := by          left          exact ⟨by rw [hz_re, l.h0], abs_zim_le⟩        exact extract_order G l.Rboundary hG_mero hG_bdd hz_Rb      | succ n_pred =>        have hz_L : z ∈ l.L := by          use n_pred + 1          exact ⟨by omega, hz_re, abs_zim_le⟩        exact combine_orders (extract_order G_circ l.L hGc_mero hGc_L hz_L)                             (extract_order G_star l.L hGs_mero hGs_L hz_L)    · have hz_Rb : z ∈ l.Rboundary := by        right        exact ⟨hz_re.2, by simpa [hz_im] using l.hT.le⟩      exact extract_order G l.Rboundary hG_mero hG_bdd hz_Rb    · have hz_Rb : z ∈ l.Rboundary := by        left        exact ⟨hz_re, abs_zim_le⟩      exact extract_order G l.Rboundary hG_mero hG_bdd hz_Rb  have h_prod_eq : (fun s ↦ G s * (x : ℂ) ^ s) = G * (fun s : ℂ ↦ (x : ℂ) ^ s) := rfl  have h_prod_order : meromorphicOrderAt (fun s ↦ G s * (x : ℂ) ^ s) z = meromorphicOrderAt G z := by    rw [h_prod_eq, meromorphicOrderAt_mul hG_mero hpow_mero, hpow_order, add_zero]  have h_pole_contra : meromorphicOrderAt (fun s ↦ G s * (x : ℂ) ^ s) z < 0 := hz_pole  rw [h_prod_order] at h_pole_contra  exact not_lt.mpr h_nonneg_G h_pole_contra