CH2.lemma_5_1_h

@[blueprint  "ch2-lemma-5-1-h"  (title := "$C_{n,1}^+ \\to C$ (CH2 Lemma 5.1, contour limit)")  (statement := /--  As $n \to \infty$ (so $\sigma_n \to -\infty$), the integral of $G^\star x^s$ over $C_{n,1}^+$  converges to its integral over the full contour $C$:  $$ \lim_{n\to\infty} \int_{C_{n,1}^+} G^\star(s) x^s\, ds = \int_C G^\star(s) x^s\, ds. $$ -/)  (proof := /-- $C_{n,1}^+$ differs from $C$ (truncated at height $\delta$) only in its horizontal  segment $1 + i\delta \to \sigma_n + i\delta$, which exhausts the ray $1 + i\delta \to -\infty + i\delta$, and its  vertical segment $\sigma_n + i\delta \to \sigma_n + iT$, which vanishes --- both as in  \ref{ch2-lemma-5-1-e}, \ref{ch2-lemma-5-1-f}, here at height $\delta$, using boundedness of  $G^\star x_0^s$ on $L$ and on $C$. -/)  (latexEnv := "sublemma")  (discussion := 1455)]theorem lemma_5_1_h (hx₀ : 1 ≤ x₀) (hx : x₀ < x)    (hG_star_mero : MeromorphicOn G_star l.R)    (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) :  Filter.Tendsto (fun n ↦ l.intCn1Plus n (fun s ↦ G_star s * (x : ℂ) ^ s)) Filter.atTop    (nhds (l.intC (fun s ↦ G_star s * (x : ℂ) ^ s))) := by  let F : ℂ → ℂ := fun s ↦ G_star s * (x : ℂ) ^ s  have h_meas_mul : AEStronglyMeasurable (fun r : ℝ ↦ G_star (r + l.δ * Complex.I) * (x : ℂ) ^ (r + l.δ * Complex.I))    (MeasureTheory.volume.restrict (Set.Iic 1)) := aestronglyMeasurable_horizontal_path_mul_cpow_of_meromorphic      l G_star x₀ x l.δ hx₀ hx (fun z hz ↦ l.admissible_contour_subset_R (Or.inl hz)) hG_star_mero      fun z hz ↦ meromorphicOrderAt_nonneg_on_of_bounded l hx₀ l.admissible_contour_subset_R hG_star_mero hGs_contour z (Or.inl hz)  have h_meas : AEStronglyMeasurable (fun r : ℝ ↦ F ((r : ℂ) + l.δ * Complex.I))        (MeasureTheory.volume.restrict (Set.Iic 1)) := by simpa [F] using h_meas_mul  have h_int_ray : IntegrableOnHRay l.δ 1 F := by    unfold IntegrableOnHRay    obtain ⟨M, hM⟩ := hGs_contour    let C : ℝ := max M 0    have hx₀_pos : 0 < x₀ := by linarith    have hx_pos : 0 < x := by linarith    have hratio_pos : 0 < x / x₀ := div_pos hx_pos hx₀_pos    have hlog_ratio_pos : 0 < Real.log (x / x₀) := Real.log_pos (by rw [one_lt_div hx₀_pos]; linarith)    have h_int_bound :        IntegrableOn (fun r : ℝ ↦ C * Real.exp (Real.log (x / x₀) * r)) (Set.Iic 1) :=      (integrableOn_exp_mul_Iic hlog_ratio_pos 1).const_mul C    have h_bound : ∀ r ∈ Set.Iic (1 : ℝ), ‖F ((r : ℂ) + l.δ * Complex.I)‖ ≤ C * Real.exp (Real.log (x / x₀) * r) := by      intro r hr      have hr' : r ≤ 1 := by simpa using hr      have hz_ac : (r : ℂ) + l.δ * Complex.I ∈ l.admissible_contour := by        left        exact ⟨by simpa using hr', by simp⟩      simpa [F, C] using norm_G_mul_cpow_le_of_base_bound G_star x₀ x l.δ r M hx₀ hx ((hM _ hz_ac).1)    exact h_int_bound.mono' h_meas <| (ae_restrict_iff' measurableSet_Iic).mpr <| ae_of_all _ (fun r hr ↦ h_bound r hr)  have h_horiz :      Filter.Tendsto (fun n : ℕ ↦ intHSeg l.δ 1 (l.σ n) F) Filter.atTop        (nhds (-intHRay l.δ 1 F)) := by    have h_symm : ∀ n, intHSeg l.δ 1 (l.σ n) F = - intHSeg l.δ (l.σ n) 1 F :=      fun n ↦ by unfold intHSeg; rw [intervalIntegral.integral_symm]    have h_seq_eq : (fun n ↦ intHSeg l.δ 1 (l.σ n) F) = (fun n ↦ - intHSeg l.δ (l.σ n) 1 F) :=      funext fun n ↦ h_symm n    have h_tendsto_ray : Filter.Tendsto (fun n ↦ intHSeg l.δ (l.σ n) 1 F) Filter.atTop (nhds (intHRay l.δ 1 F)) :=      MeasureTheory.intervalIntegral_tendsto_integral_Iic 1 h_int_ray l.hlim    rw [h_seq_eq]    simpa using h_tendsto_ray.neg  have h_vert : Filter.Tendsto (fun n : ℕ ↦ intVSeg (l.σ n) l.δ l.T F) Filter.atTop (nhds 0) := by    simpa [F] using intVSeg_tendsto_zero_of_bounded_on_L l G_star x₀ x l.δ l.T hx₀ hx        (by rw [abs_of_nonneg l.hδ.1.le]; linarith [l.hδ.2, l.hT]) le_rfl        (by linarith [l.hδ.1, l.hδ.2, l.hT]) hGs_L  have h_sum : Filter.Tendsto (fun n : ℕ ↦ intVSeg 1 0 l.δ F + (intHSeg l.δ 1 (l.σ n) F + intVSeg (l.σ n) l.δ l.T F))        Filter.atTop (nhds (intVSeg 1 0 l.δ F + (-intHRay l.δ 1 F + 0))) :=        Filter.Tendsto.add tendsto_const_nhds (Filter.Tendsto.add h_horiz h_vert)  simpa [LadderParams.intCn1Plus, LadderParams.intC, F, sub_eq_add_neg, add_assoc] using h_sum