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.
Laurent series split into regular and principal parts
Statement
Let
be a convergent Laurent series on an annulus. Then:
- the regular part converges locally uniformly on every smaller disc , and on all of when ;
- the principal part (The principal part of a Laurent series) converges locally uniformly on every set ;
- on the original annulus, is the sum of these two subseries.
Moreover, the regular and principal parts are uniquely determined by the Laurent coefficients.
Facts & Assumptions
Given: A Laurent expansion on .
Laurent expansions exist on annuli and converge locally uniformly there (Laurent expansion on an annulus).
Each Laurent coefficient is uniquely determined by the function on the annulus (Laurent coefficients are given by contour integrals and are unique).
Proof
Let and choose with ; the coefficient formula gives for , where , so for .
Let and choose with ; the coefficient formula gives for , where , so for .
On the original annulus, [L1] gives that the Laurent series converges to , and by definition that series is the sum of its nonnegative-power and negative-power subseries. So there.
Uniqueness of the Laurent coefficients from [L2] makes both subseries unique term by term.
The geometric majorant in step 1.1 converges, so the regular part converges uniformly on ; since was arbitrary, the convergence is locally uniform on the disc of radius , and when it is locally uniform on every bounded disc.
The geometric majorant in step 1.2 converges, so the principal part converges uniformly on ; since was arbitrary, the convergence is locally uniform on the exterior region .
Steps 2.1, 2.2, 1.3, and 1.4 are exactly the claimed decomposition.
Depends on
Used by
Dependency tree · two levels
13 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. 5 §1.3 (standard reference, not scraped)
- Jeremy Orloff, MIT 18.04 Topic 7: Taylor and Laurent Series (standard reference, not scraped)