Weighted argument principle on a rectangle, with poles: $\frac{1}{2\pi i}\oint g\, \frac{f'}{f} = \sum_\rho m_\rho g(\rho) - \sum_p m_p g(p)$

Let $z, w \in \mathbb{C}$ with $\operatorname{Re} z \le \operatorname{Re} w$ and $\operatorname{Im} z \le \operatorname{Im} w$, and let $R = [\operatorname{Re} z, \operatorname{Re} w] \times [\operatorname{Im} z, \operatorname{Im} w]$ be the closed rectangle they span. Let $Z, P$ be disjoint finite sets of complex numbers with every $p \in P$ interior to $R$, and let $f, g : \mathbb{C} \to \mathbb{C}$ satisfy:

• $f$ is analytic on a neighbourhood of every point of $R \setminus P$, and $g$ is analytic on a neighbourhood of every point of $R$;
• $f$ does not vanish on the boundary of the rectangle;
• on $R \setminus P$, the zeros of $f$ are exactly the elements of $Z$, and $Z \subseteq R$;
• at each $p \in P$, $f$ has a pole-type singularity of order $m(p)$: for some $c_p \ne 0$, $(s - p)^{m(p)} f(s) \to c_p$ as $s \to p$ (along the punctured neighbourhood filter).

Statement. Writing $\frac{1}{2\pi i}\oint_{\partial R}$ for the normalized rectangle contour integral (RectangleIntegral'),

where $\operatorname{ord}_\rho(f)$ is the order of vanishing of $f$ at $\rho$ (analyticOrderNatAt).

This weighted argument principle with poles is the central contour-integration tool of the project, in the module Zeta23.Analytic.RectangleLogDeriv. It is consumed by Zeta23.RvM.rectangleIntegralPrime_logDeriv_completedZeta_eq_Ncount — the contour-integral evaluation behind the Riemann–von Mangoldt formula for $N(T)$, applied to the completed zeta function with its poles at $0$ and $1$ — and by Zeta23.WeilEF.rectangle_identity, the contour identity underlying the Weil-type explicit formula.