CH2.prop_5_2_b

@[blueprint  "ch2-prop-5-2-b"  (title := "Proposition 5.2: bound on the $C_\\infty$ integral")  (statement := /--  On the rays of $C_\infty$, $z(r \pm iT) = \pm 1 + i\,\frac{1-r}{T}$, so  $|\Phi^\varepsilon_\lambda(z(s))| \leq \frac{1-r}{T}$ (CH2 Lemma 4.3); substituting $t = 1 - r$,  $$ \left\| \frac{1}{2\pi i}\int_{C_\infty} G(s) x^s\, ds \right\| \leq \frac{1}{2\pi} \cdot \frac{1}{T} \sum_{\xi = \pm 1} \int_0^\infty t\, |F(1 - t + i\xi T)|\, x^{1-t}\, dt. $$ -/)  (proof := /-- $|\Phi^\varepsilon_\lambda(\pm 1 + ir')| \leq |r'|$ (CH2 Lemma 4.3), $|x^s| = x^{\Re s}$. -/)  (latexEnv := "sublemma")  (discussion := 1458)]theorem prop_5_2_b    (hF_mero : MeromorphicOn F l.R)    (hF_symm : ConjSymm F)    (hlam : lam ≠ 0) (hε : ε = 1 ∨ ε = -1)    (hx₀ : 1 ≤ x₀)    (hF_bdd : IsBoundedNoPolesOn (fun s ↦ F s * (x₀ : ℂ) ^ s)      (l.Rboundary ∪ l.admissible_contour ∪ l.L))    (hx : x₀ < x)    (hfin : {z ∈ l.R \ l.RC |        meromorphicOrderAt (fun s ↦ Phi_lambda lam ε (l.zOf s) * F s * (x : ℂ) ^ s) z < 0}.Finite)    (hsimple : HasSimplePolesOn (fun s ↦ Phi_lambda lam ε (l.zOf s) * F s * (x : ℂ) ^ s) l.R)    (hsimple_circ :        HasSimplePolesOn          (fun s ↦ Phi_circ |lam| ε ((Real.sign lam : ℂ) * l.zOf s) * F s * (x : ℂ) ^ s) l.R) :    ‖(2 * (π : ℂ) * Complex.I)⁻¹ *        l.intCinf (fun s ↦ Phi_lambda lam ε (l.zOf s) * F s * (x : ℂ) ^ s)‖ ≤      (1 / (2 * π)) * ((1 / l.T) *        ((∫ t in Set.Ioi (0 : ℝ), t * ‖F (1 - t + l.T * Complex.I)‖ * x ^ (1 - t)) +          ∫ t in Set.Ioi (0 : ℝ), t * ‖F (1 - t - l.T * Complex.I)‖ * x ^ (1 - t))) := by  have _ := hF_symm  have _ := hfin  have _ := hsimple  have _ := hsimple_circ  let G : ℂ → ℂ := fun s ↦ Phi_lambda lam ε (l.zOf s) * F s * (x : ℂ) ^ s  let Itop : ℝ :=    ∫ t in Set.Ioi (0 : ℝ), t * ‖F (1 - t + l.T * Complex.I)‖ * x ^ (1 - t)  let Ibot : ℝ :=    ∫ t in Set.Ioi (0 : ℝ), t * ‖F (1 - t - l.T * Complex.I)‖ * x ^ (1 - t)  obtain ⟨M, hM⟩ := hF_bdd  have hF_Rbd : IsBoundedNoPolesOn (fun s ↦ F s * (x₀ : ℂ) ^ s) l.Rboundary := by    exact ⟨M, fun z hz ↦ hM z (by simp [hz])⟩  have hx_pos : 0 < x := by linarith  have htop :      ‖intHRay l.T 1 G‖ ≤ (1 / l.T) * Itop := by    have hweighted :        ‖intHRay l.T 1 G‖ ≤          ∫ r in Set.Iic (1 : ℝ), ((1 - r) / l.T) *            ‖F ((r : ℂ) + l.T * Complex.I) *              (x : ℂ) ^ ((r : ℂ) + l.T * Complex.I)‖ := by      simpa [G] using        norm_intHRay_Phi_lambda_le_weighted (l := l) (F := F) (lam := lam) (ε := ε)          (x₀ := x₀) (x := x) l.T hx₀ hx (abs_of_nonneg l.hT.le) hF_mero hF_Rbd          (ae_norm_Phi_lambda_top_hray_le (l := l) (lam := lam) (ε := ε) hlam hε)    have htransport :=      integral_weighted_F_mul_cpow_hray_eq_Ioi (l := l) (F := F) (x := x) l.T hx_pos    exact hweighted.trans (le_of_eq (by simpa [Itop] using htransport))  have hbot :      ‖intHRay (-l.T) 1 G‖ ≤ (1 / l.T) * Ibot := by    have hweighted :        ‖intHRay (-l.T) 1 G‖ ≤          ∫ r in Set.Iic (1 : ℝ), ((1 - r) / l.T) *            ‖F ((r : ℂ) + (-l.T) * Complex.I) *              (x : ℂ) ^ ((r : ℂ) + (-l.T) * Complex.I)‖ := by      simpa [G] using        norm_intHRay_Phi_lambda_le_weighted (l := l) (F := F) (lam := lam) (ε := ε)          (x₀ := x₀) (x := x) (-l.T) hx₀ hx          (by rw [abs_of_nonpos (neg_nonpos.mpr l.hT.le)]; ring)          hF_mero hF_Rbd          (ae_norm_Phi_lambda_bot_hray_le (l := l) (lam := lam) (ε := ε) hlam hε)    have htransport :=      integral_weighted_F_mul_cpow_hray_eq_Ioi (l := l) (F := F) (x := x) (-l.T) hx_pos    exact hweighted.trans (le_of_eq (by simpa [Ibot, sub_eq_add_neg] using htransport))  have hCinf :      ‖l.intCinf G‖ ≤ (1 / l.T) * Itop + (1 / l.T) * Ibot := by    unfold LadderParams.intCinf    calc      ‖intHRay l.T 1 G - intHRay (-l.T) 1 G‖          ≤ ‖intHRay l.T 1 G‖ + ‖intHRay (-l.T) 1 G‖ := norm_sub_le _ _      _ ≤ (1 / l.T) * Itop + (1 / l.T) * Ibot := add_le_add htop hbot  have hfactor :      ‖(2 * (π : ℂ) * Complex.I)⁻¹‖ = (1 / (2 * π) : ℝ) := by    rw [norm_inv, norm_mul, norm_mul, Complex.norm_ofNat, norm_real, Real.norm_eq_abs,      Complex.norm_I, mul_one, abs_of_pos Real.pi_pos]    ring  have hfactor_nonneg : 0 ≤ (1 / (2 * π) : ℝ) := by positivity  calc    ‖(2 * (π : ℂ) * Complex.I)⁻¹ *        l.intCinf (fun s ↦ Phi_lambda lam ε (l.zOf s) * F s * (x : ℂ) ^ s)‖        = (1 / (2 * π) : ℝ) * ‖l.intCinf G‖ := by          rw [norm_mul, hfactor]    _ ≤ (1 / (2 * π) : ℝ) * ((1 / l.T) * Itop + (1 / l.T) * Ibot) :=      mul_le_mul_of_nonneg_left hCinf hfactor_nonneg    _ = (1 / (2 * π)) * ((1 / l.T) * (Itop + Ibot)) := by ring