Perron.residuePull1

@[blueprint  "residuePull1"  (title := "residuePull1")  (statement := /--  For $x>1$ (of course $x>0$ would suffice) and $\sigma>0$, we have  $$  \frac1{2\pi i}  \int_{(\sigma)}\frac{x^s}{s(s+1)}ds =1  +  \frac 1{2\pi i}  \int_{(-1/2)}\frac{x^s}{s(s+1)}ds.  $$  -/)  (proof := /--  We pull to a square with corners at $-c-i*c$ and $c+i*c$ for $c>0$  sufficiently small.  By Lemma \ref{residueAtZero}, the integral over this square is equal to $1$.  -/)  (latexEnv := "lemma")]lemma residuePull1 (x_gt_one : 1 < x) (σ_pos : 0 < σ) :    VerticalIntegral' (f x) σ = 1 + VerticalIntegral' (f x) (-1 / 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 (-1 / 2) σ ×ℂ univ \ {0}) :=    (isHolomorphicOn xpos).mono fun s ⟨⟨⟨_, _⟩, _⟩, hs0⟩ hc ↦ hc.casesOn      (fun hc ↦ hs0 hc) (fun hc ↦ by linarith [show s.re = -1 from congrArg _ hc])  have := (residueAtZero 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 linarith) (by linarith))  obtain ⟨c, hcf, hc⟩ := this.exists_mem  obtain ⟨ε, hε, hεc⟩ := Metric.mem_nhdsWithin_iff.mp hcf  obtain hε := hc (ε/2)    (hεc ⟨mem_ball_iff_norm.mpr (by simp [abs_of_pos hε, hε]), half_pos hε⟩)  rw [VerticalIntegral', ← smul_sub, hε.2, ← RectangleIntegral', add_zero, add_zero, hε.1]