Adapted from PNT+ by Alex Kontorovich and Terence Tao: ResidueCalcOnRectangles.lean and RectangleArgumentPrinciple.lean, commit be5e07e04cde20c5ceabf63759bd097a9c88173f (Apache-2.0).

theorem NumberField.Odlyzko.exists_analytic_logDeriv_remainder_of_meromorphicOrderAt {f : ℂ → ℂ} {p : ℂ} {n : ℤ} (hf : MeromorphicAt f p) (hord : meromorphicOrderAt f p = ↑n) : ∃ (g : ℂ → ℂ), AnalyticAt ℂ g p ∧ (logDeriv f - fun (s : ℂ) => ↑n / (s - p)) =ᶠ[nhdsWithin p {p}ᶜ] g