RectangleIntegral_tendsTo_UpperU

@[blueprint  (title := "RectangleIntegral-tendsTo-UpperU")  (statement := /--  Let $\sigma,\sigma' \in \mathbb{R}$, and $f : \mathbb{C} \to \mathbb{C}$ such that  the vertical integrals $\int_{(\sigma)}f(s)ds$ and $\int_{(\sigma')}f(s)ds$ exist and  the horizontal integral $\int_{(\sigma)}^{\sigma'}f(x + yi)dx$ vanishes as $y \to \pm \infty$.  Then the limit of rectangle integrals  $$\int_{\sigma+iT}^{\sigma'+iU}f(s)ds$$  as $U\to\infty$ is the ``UpperUIntegral'' of $f$.  -/)  (proof := /-- Almost by definition. -/)  (proofUses := ["RectangleIntegral", "UpperUIntegral"])  (latexEnv := "lemma")]lemma RectangleIntegral_tendsTo_UpperU {σ σ' T : ℝ} {f : ℂ → ℂ}    (htop : Tendsto (fun (y : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + y * I)) atTop (𝓝 0))    (hleft : Integrable (fun (y : ℝ) ↦ f (σ + y * I)))    (hright : Integrable (fun (y : ℝ) ↦ f (σ' + y * I))) :    Tendsto (fun (U : ℝ) ↦ RectangleIntegral f (σ + I * T) (σ' + I * U)) atTop      (𝓝 (UpperUIntegral f σ σ' T)) := by  have h_re  (s : ℝ) (t : ℝ) : (s  + I * t).re = s  := by simp  have h_im  (s : ℝ) (t : ℝ) : (s  + I * t).im = t  := by simp  have hbot : Tendsto (fun (_ : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + T * I)) atTop      (𝓝 <| ∫ (x : ℝ) in σ..σ', f (x + T * I)) := by exact tendsto_const_nhds  have hvert (s : ℝ) (int : Integrable (fun (y : ℝ) ↦ f (s + y * I))) :      Tendsto (fun (U : ℝ) ↦ I * ∫ (y : ℝ) in T..U, f (s + y * I)) atTop        (𝓝 <| I * ∫ (y : ℝ) in Ioi T, f (s + y * I)) := by    exact (intervalIntegral_tendsto_integral_Ioi T int.restrict tendsto_id).const_smul I  have := ((hbot.sub htop).add (hvert σ' hright)).sub (hvert σ hleft)  simpa only [RectangleIntegral, UpperUIntegral, h_re, h_im, sub_zero,    ← integral_Ici_eq_integral_Ioi]