Perron.residuePull2

@[blueprint  "residuePull2"  (title := "residuePull2")  (statement := /--  For $x>1$, we have  $$  \frac1{2\pi i}  \int_{(-1/2)}\frac{x^s}{s(s+1)}ds = -1/x +  \frac 1{2\pi i}  \int_{(-3/2)}\frac{x^s}{s(s+1)}ds.  $$  -/)  (proof := /-- Pull contour from $(-1/2)$ to $(-3/2)$. -/)  (latexEnv := "lemma")]lemma residuePull2 (x_gt_one : 1 < x) :    VerticalIntegral' (fun s ↦ x ^ s / (s * (s + 1))) (-1 / 2)    = -1 / x + VerticalIntegral' (fun s ↦ x ^ s / (s * (s + 1))) (-3 / 2) := by  apply eq_add_of_sub_eq  have xpos : 0 < x := zero_lt_one.trans x_gt_one  have hf : HolomorphicOn (f x) (Icc (-3 / 2) (-1 / 2) ×ℂ univ \ {-1}) :=    (isHolomorphicOn xpos).mono fun s ⟨⟨⟨_, _⟩, _⟩, hs1⟩ hc ↦ hc.casesOn      (fun hc ↦ by linarith [show s.re = 0 from congrArg _ hc]) (fun hc ↦ hs1 hc)  have := (residueAtNegOne xpos).and <| verticalIntegral_sub_verticalIntegral_eq_squareIntegral    (by simpa using ⟨by linarith, by linarith⟩) hf    (tendsto_zero_Lower xpos _ _) (tendsto_zero_Upper xpos _ _)    (isIntegrable xpos (by norm_num) (by norm_num))    (isIntegrable xpos (by norm_num) (by norm_num))  obtain ⟨c, hcf, hc⟩ := this.exists_mem  obtain ⟨ε, hε, hεc⟩ := Metric.mem_nhdsWithin_iff.mp hcf  replace hε := hc (ε/2)    (hεc ⟨mem_ball_iff_norm.mpr (by simp [abs_of_pos, hε]), half_pos hε⟩)  rw [VerticalIntegral', ← smul_sub, hε.2, ← RectangleIntegral', neg_div, one_div,    ← ofReal_inv]  exact hε.1