Perron.residueAtNegOne

@[blueprint  "residueAtNegOne"  (title := "residueAtNegOne")  (statement := /--  Let $x>0$. Then for all sufficiently small $c>0$, we have that  $$  \frac1{2\pi i}  \int_{-c-i*c-1}^{c+ i*c-1}\frac{x^s}{s(s+1)}ds = -\frac1x.  $$  -/)  (proof := /-- Compute the integral. -/)  (latexEnv := "lemma")]lemma residueAtNegOne (xpos : 0 < x) : ∀ᶠ (c : ℝ) in 𝓝[>] 0,    RectangleIntegral' (f x) (-c - c * I - 1) (c + c * I - 1) = -x⁻¹ := by  filter_upwards [Ioo_mem_nhdsGT (by linarith : (0 : ℝ) < 1 / 2), diffBddAtNegOne xpos]  intro c hc bddAbove  obtain ⟨cpos, _⟩ := hc  have h_mem {s : ℂ} (hs : s ∈ Square (-1) c) :      -c ≤ s.re + 1 ∧ s.re + 1 ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c := by    rw [Square, mem_Rect (by simpa using by linarith) (by simp [cpos.le])] at hs    simpa using hs  have RectSub : Square (-1) c \ {-1} ⊆ {0, -1}ᶜ := by    refine fun s ⟨hs, hs1⟩ ↦ not_or.mpr ⟨?_, hs1⟩    simpa [Complex.ext_iff] using fun _ _ ↦ by linarith [h_mem hs]  have fHolo : HolomorphicOn (f x) (Square (-1) c \ {-1}) := (isHolomorphicOn xpos).mono RectSub  have f1Holo :      HolomorphicOn ((f x) - (fun (s : ℂ) ↦ -x⁻¹ / (s + 1))) (Square (-1) c \ {-1}) := by    refine fHolo.sub <| (differentiableOn_const _).neg.div ?_      fun x hx ↦ sPlusOneNeZero hx.2    exact differentiableOn_id.add (differentiableOn_const 1)  have RectMemNhds : Square (-1) c ∈ 𝓝 (-1) := square_mem_nhds (-1) (ne_of_gt cpos)  obtain ⟨g, gHolo, g_eq_fDiff⟩ :=    existsDifferentiableOn_of_bddAbove RectMemNhds f1Holo bddAbove  simp_rw [Square] at fHolo gHolo RectMemNhds  refine ResidueTheoremOnRectangleWithSimplePole ?_ ?_ RectMemNhds gHolo ?_  · simpa using cpos.le  · simpa using cpos.le  · convert! g_eq_fDiff using 3; simp