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.
Mittag-Leffler on the complex plane
Statement
Let be a discrete set, listed so that , and let be a prescribed principal part at for each . Then there is a meromorphic function on whose principal part at is for every .
Facts & Assumptions
Given: A discrete set with and prescribed principal parts .
A prescribed principal part is a finite negative Laurent polynomial at the chosen point (The principal part at an isolated singularity).
On a compact set with connected complement, every holomorphic function on a neighbourhood is uniformly approximable by polynomials (Runge polynomial approximation when the complement is connected).
Proof
Choose radii so that and is finite for every . [given, L1, choose] Put Then each is finite and . For , the finite sum is holomorphic on a neighbourhood of , because every pole it carries lies outside that disc. Set likewise .
By [L2], for each choose a polynomial such that [L2, step 1.1, construct] Put and for . Then every is meromorphic on , has the same principal parts as the finitely many with , and is holomorphic on .
Fix a compact set . Choose with [step 2.1, choose, algebra, discharge-construct] . For every , one has , so step 2.1 gives . Hence converges uniformly on . Near any point , all terms except are holomorphic, so the sum is meromorphic on and has principal part at .
Depends on
Used by
Dependency tree · two levels
5 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
- M. Weber, Complex Analysis, Theorem 3.3.2 (standard reference, not scraped)
- J. Lebl, Guide to Cultivating Complex Analysis, §9.4 (standard reference, not scraped)