CH2.lemma_5_1_e

@[blueprint  "ch2-lemma-5-1-e"  (title := "The $C_\\infty$ limit (CH2 Lemma 5.1, eq. 5)")  (statement := /--  As $n \to \infty$ (so $\sigma_n \to -\infty$), the top segment of $C_n^+$ together with the  bottom segment of $C_n^-$ converge to the contour $C_\infty$:  $$ \lim_{n\to\infty} \left( \int_{\sigma_n + iT}^{1 + iT} + \int_{1 - iT}^{\sigma_n - iT} \right) G(s) x^s\, ds = \int_{C_\infty} G(s) x^s\, ds. $$ -/)  (proof := /-- As $\sigma_n \to -\infty$ the truncated horizontal segments exhaust the rays of $C_\infty$; uses boundedness of $G x_0^s$ on $\partial R$ and $x > x_0$. -/)  (latexEnv := "sublemma")  (discussion := 1452)]theorem lemma_5_1_e    (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_contour : IsBoundedNoPolesOn (fun s ↦ G_circ s * (x₀ : ℂ) ^ s) l.admissible_contour)    (hGs_contour : IsBoundedNoPolesOn (fun s ↦ G_star s * (x₀ : ℂ) ^ s) l.admissible_contour)    (hx : x₀ < x) :    Filter.Tendsto      (fun n ↦ intHSeg l.T (l.σ n) 1 (fun s ↦ G s * (x : ℂ) ^ s) +        intHSeg (-l.T) 1 (l.σ n) (fun s ↦ G s * (x : ℂ) ^ s))      Filter.atTop (nhds (l.intCinf (fun s ↦ G s * (x : ℂ) ^ s))) := by  have h_int_top : IntegrableOnHRay l.T 1 (fun s ↦ G s * (x : ℂ) ^ s) :=    G_mul_cpow_integrable_hray l hG hG_circ_mero hG_star_mero x₀ x l.T hx₀ hx (abs_of_nonneg l.hT.le) hG_bdd hGc_contour hGs_contour  have h_int_bot : IntegrableOnHRay (-l.T) 1 (fun s ↦ G s * (x : ℂ) ^ s) :=    G_mul_cpow_integrable_hray l hG hG_circ_mero hG_star_mero x₀ x (-l.T) hx₀ hx (by rw [abs_of_nonpos (neg_nonpos.mpr l.hT.le)]; ring) hG_bdd hGc_contour hGs_contour  have h_symm : ∀ n, intHSeg (-l.T) 1 (l.σ n) (fun s ↦ G s * (x : ℂ) ^ s) = - intHSeg (-l.T) (l.σ n) 1 (fun s ↦ G s * (x : ℂ) ^ s) :=    fun n ↦ by unfold intHSeg; rw [intervalIntegral.integral_symm]  have h_seq_eq : (fun n ↦ intHSeg l.T (l.σ n) 1 (fun s ↦ G s * (x : ℂ) ^ s) + intHSeg (-l.T) 1 (l.σ n) (fun s ↦ G s * (x : ℂ) ^ s)) =      (fun n ↦ intHSeg l.T (l.σ n) 1 (fun s ↦ G s * (x : ℂ) ^ s) - intHSeg (-l.T) (l.σ n) 1 (fun s ↦ G s * (x : ℂ) ^ s)) :=    funext fun n ↦ by rw [h_symm n, sub_eq_add_neg]  have h_tendsto_top := MeasureTheory.intervalIntegral_tendsto_integral_Iic 1 h_int_top l.hlim  have h_tendsto_bot := MeasureTheory.intervalIntegral_tendsto_integral_Iic 1 h_int_bot l.hlim  rw [h_seq_eq]  exact h_tendsto_top.sub h_tendsto_bot