TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-28

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The weighted argument principle

Statement

Let $Ω \subseteq C$ be open, let $f$ be meromorphic on $Ω$ , let $Γ$ be admissible for the residue theorem in $Ω$ , suppose $f (z) \neq 0$ for every $z \in Γ^{*}$ , and let $g$ be holomorphic on $Ω$ . Then

$\frac{1}{2 π i} \int_{Γ} g (z) \frac{f^{'} (z)}{f (z)} d z = \sum_{a \in Z (f)} n (Γ, a) {ord}_{a} (f) g (a) - \sum_{b \in P (f)} n (Γ, b) {ord}_{b}^{p o l e} (f) g (b),$

and only finitely many terms are nonzero.

Facts & Assumptions

Given: An open set $Ω$ , a meromorphic function $f$ on $Ω$ , an admissible cycle $Γ$ with $f \neq 0$ on $Γ^{*}$ , and a holomorphic function $g$ on $Ω$ .

[L1]

The logarithmic derivative has residue $m$ at a zero of order $m$ and residue $- m$ at a pole of order $m$ (The logarithmic derivative has residue equal to local order).

[L2]

The unweighted argument principle already shows that only finitely many zeros and poles of $f$ have nonzero index with respect to $Γ$ (The argument principle for an admissible null-homologous cycle).

[L3]

The residue theorem sums the indexed residues of an admissible meromorphic function over $Γ$ (The residue theorem for a null-homologous cycle).

Proof

technique · direct

1.1

Put $h (z) : = g (z) f^{'} (z) / f (z)$ . Away from the zeros and poles of $f$ , the function $f^{'} / f$ is holomorphic, so $h$ is holomorphic there as well. At a zero or pole $c$ of $f$ , the function $g$ is holomorphic and therefore admits the expansion $g (z) = g (c) + (z - c) u (z)$ near $c$ for some holomorphic $u$ . Multiplying that by the principal-part decomposition from [L1] shows $Res (h, c) = g (c) Res ⁣ (\frac{f^{'}}{f}, c) .$

givenL1algebra

2.1

Step 1.1 and [L1] therefore give $Res (h, a) = g (a) {ord}_{a} (f)$ at each zero $a$ of $f$ , and $Res (h, b) = - g (b) {ord}_{b}^{p o l e} (f)$ at each pole $b$ of $f$ . By [L2], only finitely many such points have nonzero index with respect to $Γ$ .

step 1.1L1L2

3.1

Applying [L3] to $h$ and substituting the residue values from step 2.1 gives the displayed weighted sum formula.

step 2.1L3∎

Depends on

Used by

A contour formula for a locally single-valued holomorphic inverse Theorem

Dependency tree · two levels

17 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. Lebl, Guide to Cultivating Complex Analysis, §5.4 (standard reference, not scraped)
R. W. Howell and J. H. Mathews, Complex Analysis, §8.7 (standard reference, not scraped)