Perron.residueAtZero

@[blueprint  "residueAtZero"  (title := "residueAtZero")  (statement := /--  Let $x>0$. Then for all sufficiently small $c>0$, we have that  $$  \frac1{2\pi i}  \int_{-c-i*c}^{c+ i*c}\frac{x^s}{s(s+1)}ds = 1.  $$  -/)  (latexEnv := "lemma")]lemma residueAtZero (xpos : 0 < x) : ∀ᶠ (c : ℝ) in 𝓝[>] 0,    RectangleIntegral' (f x) (-c - c * I) (c + c * I) = 1 := by  /-- For $c>0$ sufficiently small, -/  filter_upwards    [Ioo_mem_nhdsGT (by linarith : (0 : ℝ) < 1 / 2), diffBddAtZero xpos]  intro c hc bddAbove  obtain ⟨cpos, _⟩ := hc  have RectSub : Square 0 c \ {0} ⊆ {0, -1}ᶜ := by    refine fun s ⟨hs, hs0⟩ ↦ not_or.mpr ⟨hs0, ?_⟩    rw [Square, mem_Rect (by simpa using by linarith) (by simp [cpos.le])] at hs    replace hs : -c ≤ s.re ∧ s.re ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c := by simpa using hs    simpa [Complex.ext_iff] using fun h ↦ by linarith  have fHolo : HolomorphicOn (f x) (Square 0 c \ {0}) := (isHolomorphicOn xpos).mono RectSub  have f1Holo : HolomorphicOn ((f x) - (fun (s : ℂ) ↦ 1 / s)) (Square 0 c \ {0}) :=    fHolo.sub (by simpa using differentiableOn_inv.mono fun s hs ↦ hs.2)   have RectMemNhds : Square 0 c ∈ 𝓝 0 := square_mem_nhds 0 (ne_of_gt cpos)  /--  $x^s/(s(s+1))$ is equal to $1/s$ plus a function, $g$, say,  holomorphic in the whole rectangle (by Lemma \ref{diffBddAtZero}).  -/  obtain ⟨g, gHolo, g_eq_fDiff⟩ :=    existsDifferentiableOn_of_bddAbove RectMemNhds f1Holo bddAbove  simp_rw [Square, add_zero] at fHolo gHolo RectMemNhds  /-- Now apply Lemma \ref{ResidueTheoremOnRectangleWithSimplePole}. -/  refine ResidueTheoremOnRectangleWithSimplePole ?_ ?_ RectMemNhds gHolo ?_  any_goals simpa using cpos.le  convert g_eq_fDiff using 3 <;> simp [Square]