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 residue theorem for a null-homologous cycle
Statement
Let be open, let be meromorphic on with pole set , and let be admissible for the residue theorem in . Then
where only finitely many terms are nonzero.
Facts & Assumptions
Given: An open set , a meromorphic function on with pole set , and an admissible cycle in .
Only finitely many poles have nonzero index with respect to (Only finitely many singularities contribute to the residue sum of an admissible cycle).
For a sufficiently small positively oriented circle around an isolated singularity , the integral of on that circle is (The residue is the normalized small-circle integral).
If two cycles are homologous in an open set on which a function is holomorphic, then their contour integrals agree (Holomorphic integrals agree on homologous cycles).
A positively oriented circle around has index inside and outside (A circle traversed times has winding number inside and outside).
Proof
By [L1], the set is finite. For each choose so small that the closed discs are pairwise disjoint, lie in , meet no pole other than , and are disjoint from . Let be the positively oriented circle .
Put [step 1.1, L4] For every one has . Indeed, if then admissibility makes , and every lies in , so gives as well. If , then [L4] gives and for , so . Therefore and are homologous in .
The function is holomorphic on , so [L3] applied to step 2.1 yields
Each encloses only the pole , so [L2] gives Substituting this into step 3.1 proves the displayed formula. Since the set is finite, the residue sum has only finitely many nonzero terms.
Depends on
Used by
- A positively oriented circle integral is the sum of the enclosed residues Corollary
- The Basel sum is pi squared over six by a residue computation Corollary
- A rectangle contour evaluates the Gaussian cosine integral Example
- The whole-line principal value of sin x / x is pi, so the half-line integral is pi / 2 Example
- FALSE: the residue theorem applies to every cycle in the ambient domain False statement
- Cosecant residues sum an alternating rational series over the integers Theorem
- Cotangent residues sum a rational function over the integers Theorem
- Indented real-axis contours compute principal values with half-residue corrections Theorem
- Keyhole contours evaluate Mellin-type rational integrals Theorem
- Rational Fourier integrals are evaluated by residues and Jordan's lemma Theorem
- Rational improper integrals without real poles are upper-half-plane residue sums Theorem
- Trigonometric integrals become contour integrals by the unit-circle substitution Theorem
Dependency tree · two levels
43 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
- L. V. Ahlfors, Complex Analysis, 3rd ed., Ch. 4 §5.1, Theorem 17 (standard reference, not scraped)
- E. Stein and R. Shakarchi, Complex Analysis, Ch. 3 §2 (standard reference, not scraped)