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 plane domains
Statement
Let be a plane domain, let be a discrete set, and for each let be a prescribed principal part at . Then there is a meromorphic function on whose principal part at each is .
Facts & Assumptions
Given: A plane domain , a discrete set , and a prescribed principal part at each .
Every compact subset of an open Euclidean set has a compact Jordan neighbourhood still inside that open set (A compact subset of an open Euclidean set has a compact Jordan neighborhood inside that open set).
If a compact set has a pole set meeting every complementary component, then every function holomorphic on a neighbourhood of that compact set is uniformly approximable there by rational functions with poles in the chosen set (Runge approximation with a prescribed pole set).
A prescribed principal part is a finite negative Laurent polynomial (The principal part at an isolated singularity).
Proof
Choose an increasing compact exhaustion of with and . [given, L1, L3, construct] Recursively apply [L1] to choose compact Jordan neighbourhoods of the and then fill every complementary component lying entirely in . This gives an increasing exhaustion of compact subsets of such that every connected component of meets . Because is discrete, each set is finite. Let Then is meromorphic on and holomorphic on a neighbourhood of .
Fix a set meeting every connected component of . [L2, step 1.1, choose] Step 1.1 makes meet every connected component of as well. Put and . For each , apply [L2] to on a neighbourhood of and choose a rational function with poles in such that Then is meromorphic on , has the same principal parts as on , and is uniformly small on .
For a compact set , choose with [step 2.1, algebra, discharge-construct] . Then for every , step 2.1 gives . Therefore converges uniformly on . Only finitely many layers meet a given compact set, so is meromorphic on , and its principal part at each is exactly .
Depends on
Used by
Dependency tree · two levels
16 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, Theorem 9.4.1 (standard reference, not scraped)
- M. Weber, Complex Analysis, Theorem 3.3.2 and Runge Theory (standard reference, not scraped)