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.
Only finitely many singularities contribute to the residue sum of an admissible cycle
Statement
Let be meromorphic on an open set , let be its pole set, and let be admissible for the residue theorem in . Then
is a finite set.
Facts & Assumptions
Given: A meromorphic on an open set , its pole set , and an admissible cycle in .
The index of a cycle is locally constant off its trace and vanishes sufficiently far from the trace (The index of a cycle is locally constant off its trace and vanishes far from it).
The pole set of a meromorphic function is closed and discrete in the ambient open set (Poles of a meromorphic function form a closed discrete set and are at most countable).
Proof
Let By the local constancy part of [L1], is open in . The same local constancy also shows that if , then a whole neighbourhood of lies outside , so every limit point of outside the trace already lies in . Therefore .
By the far-from-the-trace clause of [L1], the set is bounded. Since the trace is compact, step 1.1 makes a bounded closed subset of , hence compact.
Because is admissible, its trace avoids the pole set. Thus [given, step 2.1, L2] ∎ The right-hand set is a closed discrete subset of the compact set by, and every closed discrete subset of a compact metric space is finite. So only finitely many poles have nonzero index.
Depends on
Used by
Dependency tree · two levels
38 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 (standard reference, not scraped)