logDerivResidue

@[blueprint  (title := "logDerivResidue")  (statement := /--  If $f$ is holomorphic in a neighborhood of $p$, and there is a simple pole at $p$, then $f'/  f$ has a simple pole at $p$ with residue $-1$:  $$ \frac{f'(s)}{f(s)} = \frac{-1}{s - p} + O(1).$$  -/)  (proof := /--  Using Theorem \ref{existsDifferentiableOn_of_bddAbove}, there is a function $g$ holomorphic  near $p$, for which $f(s) = A/(s-p) + g(s) = h(s)/ (s-p)$. Here $h(s):= A + g(s)(s-p)$ which  is nonzero in a neighborhood of $p$ (since $h$ goes to $A$ which is nonzero).  Then $f'(s) = (h'(s)(s-p) - h(s))/(s-p)^2$, and we can compute the quotient:  $$  \frac{f'(s)}{f(s)}+1/(s-p) = \frac{h'(s)(s-p) - h(s)}{h(s)} \cdot \frac{1}{(s-p)}+1/(s-p)  =  \frac{h'(s)}{h(s)}.  $$  Since $h$ is nonvanishing near $p$, this remains bounded in a neighborhood of $p$.  -/)]theorem logDerivResidue {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ}    (non_zero : ∀ x ∈ U \ {p}, f x ≠ 0)    (holc : HolomorphicOn f (U \ {p}))    (U_in_nhds : U ∈ 𝓝 p) {A : ℂ} (A_ne_zero : A ≠ 0)    (f_near_p : BddAbove (norm ∘ (f - fun s ↦ A * (s - p)⁻¹) '' (U \ {p}))) :    (deriv f * f⁻¹ + (fun s ↦ (s - p)⁻¹)) =O[𝓝[≠] p] (1 : ℂ → ℂ) :=    by      let ⟨U', ⟨a,b,c⟩⟩ := mem_nhds_iff.mp U_in_nhds      have W : (U' \ {p}) ⊆ U' := by        exact Set.sdiff_subset       have T : (U' \ {p}) ⊆ (U \ {p}) := by        exact Set.sdiff_subset_sdiff a (subset_refl _)        refine logDerivResidue' b ?_ ?_ (IsOpen.mem_nhds b c) A_ne_zero ?_      · intro x hyp_x        exact non_zero x <| T hyp_x      · exact DifferentiableOn.mono holc T      · exact (f_near_p.mono (image_mono (Set.sdiff_subset_sdiff a (subset_refl _))))