CH2.prop_5_2_a

@[blueprint  "ch2-prop-5-2-a"  (title := "Proposition 5.2: reduction to Lemma 5.1")  (statement := /--  Under the hypotheses of \ref{ch2-prop-5-2}, with $G$, $G^\circ$, $G^\star$, $z(s)$ as there, the  decomposition $G = G^\circ + \mathrm{sgn}(\Im s)\, G^\star$ holds (as $\mathrm{sgn}(\Re z(s)) =  \mathrm{sgn}(\Im s)$, since $\Re z(s) = \Im s / T$ and $T > 0$), $G^\star$ is  conjugation-antisymmetric, and the boundedness hypotheses of Lemma \ref{ch2-lemma-5-1} hold;  hence Lemma \ref{ch2-lemma-5-1} gives  $$ \frac{1}{2\pi i}\int_{1-iT}^{1+iT} G(s) x^s\, ds = \frac{1}{2\pi i}\int_{C_\infty} G(s) x^s\, ds + \frac{1}{\pi}\Im\int_C G^\star(s) x^s\, ds + \sum_{\rho \in R \setminus R_C}\mathrm{Res}_{s=\rho} G(s) x^s + \sum_{\rho \in R_C}\mathrm{Res}_{s=\rho} G^\circ(s) x^s. $$ -/)  (proof := /-- Apply Lemma \ref{ch2-lemma-5-1}. The $G^\star$ reflection is the conjugation  symmetry of $\Phi^\star$ together with $F(\bar s) = \overline{F(s)}$. For $\lambda > 0$ the rescaled  argument $\mathrm{sgn}(\lambda)\, z(s)$ has $\Im \geq 0$ on $R$, so $\Phi^\circ$, $\Phi^\star$ are  pole-free there; $\Phi^\circ$ is bounded and $\Phi^\star, \Phi_\lambda = O(|z|)$ (CH2 Lemma 4.3),  the linear growth being absorbed by the assumed bound on $z(s)\, F(s)\, x_0^s$. -/)  (latexEnv := "sublemma")  (discussion := 1457)]theorem prop_5_2_a    (hF_mero : MeromorphicOn F l.R)    (hF_symm : ConjSymm F)    (hlam : 0 < lam) (_hε : ε = 1 ∨ ε = -1)    (hx₀ : 1 ≤ x₀)    (hF_bdd : IsBoundedNoPolesOn (fun s ↦ F s * (x₀ : ℂ) ^ s)      (l.Rboundary ∪ l.admissible_contour ∪ l.L))    (hFw_bdd : IsBoundedNoPolesOn (fun s ↦ l.zOf 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.intVerticalAt 1 (fun s ↦ Phi_lambda lam ε (l.zOf s) * F s * (x : ℂ) ^ s) =      (2 * (π : ℂ) * Complex.I)⁻¹ *          l.intCinf (fun s ↦ Phi_lambda lam ε (l.zOf s) * F s * (x : ℂ) ^ s) +        (↑(π⁻¹ * (l.intC (fun s ↦ (Real.sign lam : ℂ) *            Phi_star |lam| ε ((Real.sign lam : ℂ) * l.zOf s) * F s * (x : ℂ) ^ s)).im) : ℂ) +        sumResiduesIn (fun s ↦ Phi_lambda lam ε (l.zOf s) * F s * (x : ℂ) ^ s) (l.R \ l.RC) +        l.sumResiduesLim          (fun s ↦ Phi_circ |lam| ε ((Real.sign lam : ℂ) * l.zOf s) * F s * (x : ℂ) ^ s) l.RC := by  refine lemma_5_1    (G := fun s ↦ Phi_lambda lam ε (l.zOf s) * F s)    (G_circ := fun s ↦ Phi_circ |lam| ε ((Real.sign lam : ℂ) * l.zOf s) * F s)    (G_star := fun s ↦ (Real.sign lam : ℂ) *        Phi_star |lam| ε ((Real.sign lam : ℂ) * l.zOf s) * F s)    ?hG ?hGc_mero ?hGs_mero ?hGs_symm ?hGc_symm hx₀ ?hG_bdd ?hGc_L ?hGc_contour    ?hGs_L ?hGs_contour hx ?hfin ?hsimple ?hsimple_circ  case hfin => exact hfin  case hsimple => exact hsimple  case hsimple_circ => exact hsimple_circ  -- remaining genuine subgoals (to be discharged):  case hG =>    intro s    simp only [Phi_lambda, l.sign_zOf_re]    ring  case hGc_mero =>    intro z hz    refine MeromorphicAt.mul ?_ (hF_mero z hz)    exact (Phi_circ.meromorphic |lam| ε _).comp_analyticAt (l.analyticAt_zOf _ z)  case hGs_mero =>    intro z hz    refine MeromorphicAt.mul ?_ (hF_mero z hz)    exact (MeromorphicAt.const (Real.sign lam : ℂ) z).mul      ((Phi_star.meromorphic |lam| ε _).comp_analyticAt (l.analyticAt_zOf _ z))  case hGs_symm =>    intro s    simp only []    rw [l.zOf_conj, hF_symm,      show (Real.sign lam : ℂ) * -(starRingEnd ℂ (l.zOf s)) =          -(starRingEnd ℂ ((Real.sign lam : ℂ) * l.zOf s)) by        rw [map_mul, Complex.conj_ofReal]; ring,      Phi_star_conj_neg, map_mul, map_mul, Complex.conj_ofReal]    ring  case hGc_symm =>    intro s    simp only []    have hPhi : Phi_circ |lam| ε        (-(starRingEnd ℂ ((Real.sign lam : ℂ) * l.zOf s))) =        starRingEnd ℂ (Phi_circ |lam| ε ((Real.sign lam : ℂ) * l.zOf s)) := by      unfold Phi_circ      simp only [map_mul, map_add, map_div₀, Complex.conj_ofReal, neg_mul, mul_neg,        neg_neg, coth_conj, map_one, map_ofNat, Complex.conj_I, map_neg]    rw [l.zOf_conj, hF_symm,      show (Real.sign lam : ℂ) * -(starRingEnd ℂ (l.zOf s)) =          -(starRingEnd ℂ ((Real.sign lam : ℂ) * l.zOf s)) by        rw [map_mul, Complex.conj_ofReal]        ring,      hPhi, map_mul]  case hG_bdd =>    exact isBoundedNoPolesOn_Phi_lambda_mul l hlam hx₀ hF_mero l.Rboundary_subset_R      (hF_bdd.mono (Set.subset_union_left.trans Set.subset_union_left))      (hFw_bdd.mono (Set.subset_union_left.trans Set.subset_union_left))  case hGc_L =>    exact isBoundedNoPolesOn_Phi_circ_mul l hlam hx₀ hF_mero l.L_subset_R      (hF_bdd.mono Set.subset_union_right)  case hGc_contour =>    exact isBoundedNoPolesOn_Phi_circ_mul l hlam hx₀ hF_mero l.admissible_contour_subset_R      (hF_bdd.mono (Set.subset_union_right.trans Set.subset_union_left))  case hGs_L =>    exact isBoundedNoPolesOn_Phi_star_mul l hlam hx₀ hF_mero l.L_subset_R      (hF_bdd.mono Set.subset_union_right) (hFw_bdd.mono Set.subset_union_right)  case hGs_contour =>    exact isBoundedNoPolesOn_Phi_star_mul l hlam hx₀ hF_mero l.admissible_contour_subset_R      (hF_bdd.mono (Set.subset_union_right.trans Set.subset_union_left))      (hFw_bdd.mono (Set.subset_union_right.trans Set.subset_union_left))