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 and Runge's Theorem
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Analyticity of Holomorphic Functions; Liouville and Morera
- Arc Length and Rectifiable Curves
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Variation and the Riemann–Stieltjes Integral
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Differentiability and the Cauchy–Riemann Equations
- Complex Power Series and Analytic Functions
- Connectedness
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Contour Integration
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Fubini and Change of Variables
- Function Space Topologies and the Exponential Law
- Fundamental Trigonometric Identities
- Goursat's Theorem and Cauchy's Theorem in a Convex Domain
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Infinite Products and the Weierstrass Factorisation Theorem
- Isolated Singularities and Laurent Series
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Line Integrals and the Gradient Theorem
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Partitions of Unity and Paracompactness
- pi: the Equivalent Characterizations
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Properties of the Integral and the Working FTC
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Simple Field Extensions and the Construction of the Complex Numbers
- Sine, Cosine, and the Definition of Pi
- Subspaces, Products, and Quotients
- Suprema and Infima
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Exponential Function
- The Fundamental Theorems of Calculus
- The Identity Theorem, the Maximum Principle and the Open Mapping Theorem
- The Logarithm and General Powers
- The Residue Theorem and the Evaluation of Real Integrals
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The Winding Number and the Global Cauchy Theorem
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
Runge's theorem is the approximation engine on this page. The compact-set version is built in three stages exactly as planned: a polygonal cycle enclosing the compact set, a Cauchy-integral Riemann-sum approximation with poles on that cycle, and pole pushing inside complementary components until the poles land in the chosen representative set. The connected-complement case then collapses to polynomial approximation.
Mittag-Leffler is the additive analogue. On the plane, Taylor-polynomial subtractions force convergence of the sum of principal parts; on a general plane domain, the same normal-convergence idea is driven by a Runge exhaustion. The page closes with the cotangent partial fractions and the standard divisor and quotient consequences for meromorphic functions on plane domains.
3 · Logical flowchart
4 · Definitions, theorems and proofs
The principal part at an isolated singularity
Definition
Let , let , and let be holomorphic on the punctured disc . By Laurent expansion on an annulus, the function has a Laurent expansion about on that punctured disc. By Laurent series split into regular and principal parts, this expansion splits uniquely into its regular and principal parts.
The principal part of at is the negative-power part of that Laurent expansion:
For Mittag-Leffler data, a prescribed principal part at means a finite sum
This is exactly the shape of the principal part of a pole whose order is at most , and its order is exactly when .
Remarks
The point of the adjective "prescribed" is that one starts with the negative Laurent polynomial and asks for a meromorphic function having it at . The pole order is then the largest with .
Runge pole sets for rational approximation on a compact set
Definition
Let be compact, let be an open neighbourhood of , and let be holomorphic. A subset is a Runge pole set for when every connected component of meets .
One says that is rationally approximable on with poles in when for every there is a rational function whose finite poles all lie in and whose only possible pole at is also in , such that
Remarks
If is connected, then the singleton is a Runge pole set. In that case the approximants are exactly polynomials.
Pole pushing along a chain of discs
Definition
Let be compact. A pole-pushing chain from to relative to is a finite list of closed discs such that
- for every ;
- for every .
Given , pushing the pole of along that chain to means finding a rational function with the following properties:
- is holomorphic on a neighbourhood of ;
- has at most one finite pole, namely at ;
- .
If the terminal point is declared to be , the third clause is kept and the second is replaced by "the approximant is a polynomial".
A square-grid cycle enclosing a compact set
Statement
Let , where is compact and is open. Then there is a complex chain with polygonal trace such that
- is a cycle;
- ;
- for every .
Facts & Assumptions
Given: A compact set contained in an open set .
A compact subset of an open Euclidean set has a compact Jordan neighbourhood inside that open set, and it may be taken to be a finite union of closed grid rectangles (A compact subset of an open Euclidean set has a compact Jordan neighborhood inside that open set).
The winding number of a closed contour is its continuous-argument increment divided by (The winding number is the increment of a continuous argument divided by ).
Chain integrals and indices are additive, and reversing an oriented edge negates its contribution (Chain integration and the index are additive in the chain, and reverse with it).
The index of a cycle is locally constant off its trace (The index of a cycle is locally constant off its trace and vanishes far from it).
Proof
By [L1], choose a compact Jordan set such that , and write as a finite union of closed cells from one square grid. Give every cell boundary its positive orientation. Each edge internal to then occurs twice with opposite orientations; cancel those pairs and let be the finite chain of the remaining oriented frontier edges. At every grid vertex the incoming and outgoing coefficients balance, so is a cycle. Its trace is the frontier of , hence .
Let lie on no grid line. Summing the positively oriented boundaries of all cells gives the same integral and index as , because the two orientations of every internal edge cancel by [L3]. For one grid cell , the four-edge continuous argument of makes one positive turn when and returns with zero net turn when ; hence [L2] gives in the first case and in the second. Exactly one cell containing contributes , so additivity in [L3] gives .
Fix . Choose a disc and a point on no grid line. The disc misses and is connected, so local constancy in [L4] and step 2.1 give .
Riemann sums of the Cauchy integral give rational approximation
Statement
Let , where is compact and is open, and let be holomorphic. Then for every there is a rational function whose poles lie on a finite set contained in and such that
Facts & Assumptions
Given: A compact set , an open neighbourhood of , a holomorphic function , and a tolerance .
There is a polygonal cycle with and for every (A square-grid cycle enclosing a compact set).
A cycle null-homologous in an open set satisfies the global Cauchy formula there (Cauchy's integral formula for a null-homologous cycle, Null-homologous cycles and homologous cycles in an open set).
A continuous map on a compact metric space is uniformly continuous, and the continuous image of a compact space is compact (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous, The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset).
Proof
Choose as in [L1]. Because on and , the cycle is null-homologous in and [L2] gives
Decompose into finitely many oriented line segments . For each , the function is continuous on the compact set , because . By [L3], each is uniformly continuous there, so a fine enough Riemann sum approximates uniformly in .
Summing those edgewise Riemann sums gives a rational function of the form with sample points . Choosing the mesh so that the total edgewise error is below and using step 1.1 yields .
Runge's pole-pushing lemma
Statement
Let be compact.
- If is a pole-pushing chain from to relative to , then for every there is a rational function with at most one finite pole, at , such that .
- If is such a chain and in addition for every , then for every there is a polynomial with .
Facts & Assumptions
Given: A compact set , a pole-pushing chain as in the statement, and a tolerance .
In a pole-pushing chain, each consecutive pair lies in a closed disc disjoint from (Pole pushing along a chain of discs).
Proof
Fix one disc step of the chain, say a closed disc disjoint from and two points . [given, L1] Define to be the set of points such that can be approximated uniformly on by rational functions with only pole . Certainly .
Let . Choose so that and . [step 1.1, choose, algebra] If and , then for one has , so with uniform convergence on . Therefore every rational function with only pole can be approximated uniformly on by one with only pole . Since , this shows , so is open. The same expansion with and exchanged shows that whenever is sufficiently close to , then as well. Hence is also closed in . Because the disc is connected and is nonempty, , so in particular .
If , then , and proves clause 1 with zero error. Assume . Apply step 2.1 successively to the discs of the chain, choosing the -th local error below . [step 2.1, choose, construct, cases, algebra] The triangle inequality then produces a rational function with only pole and total error below on . This proves clause 1.
For clause 2, clause 1 gives a rational function with only pole and . [step 3.1, algebra, discharge-construct] Write the principal part of at as . Because on , each factor has a power series in that converges uniformly on . Truncating those finitely many series gives a polynomial with . Then , proving the polynomial approximation.
Runge approximation with a prescribed pole set
Statement
Let be compact, let be an open neighbourhood of , let be holomorphic, and let be a Runge pole set for . Then for every there is a rational function with poles only in such that
Facts & Assumptions
Given: A compact set , a holomorphic function on a neighbourhood of , a Runge pole set , and a tolerance .
The Cauchy integral over a suitable enclosing cycle can be approximated uniformly on by rational functions with poles on that cycle (Riemann sums of the Cauchy integral give rational approximation).
A Runge pole set meets every complementary component of (Runge pole sets for rational approximation on a compact set).
A simple pole may be pushed through one complementary component to any chosen representative in that component, or to in the unbounded case (Runge's pole-pushing lemma).
Proof
By [L1], choose a rational function whose poles lie in and such that .
If , then already has no finite poles, so its poles are contained in and step 1.1 already proves the theorem. Assume from now on that .
For each pole , let be the connected component of containing it. By [L2], choose . Applying [L3] to the function inside , choose a rational function with poles only at and
Put . Then every pole of lies in , and the triangle inequality together with steps 1.1 and 3.1 gives
Runge polynomial approximation when the complement is connected
Statement
Let be compact and let be connected. If is holomorphic on a neighbourhood of , then for every there is a polynomial such that
Facts & Assumptions
Given: A compact set with connected complement and a holomorphic function on a neighbourhood of .
Runge approximation holds for every pole set meeting each complementary component (Runge approximation with a prescribed pole set).
Proof
Since is connected, the singleton meets its unique complementary component. Applying [L1] with that pole set gives rational approximants whose only possible pole is at .
If is such a rational function in lowest terms and has positive degree, then a zero of would give a finite pole of . Therefore is constant, so is a polynomial. Hence the approximants from step 1.1 are polynomials.
Runge approximation on a plane domain
Definition
Let be a plane domain, let , and let be holomorphic.
One says that is Runge-approximable on with poles in when there is a sequence of rational functions such that every finite pole of lies in , the only possible pole at infinity also lies in , and
If is connected and , this is simply polynomial approximation on .
Remarks
The compact-set theorem supplies the local pieces of this definition. The next theorem upgrades them to a single sequence on the whole domain by choosing an exhaustion.
Runge approximation on plane domains
Statement
Let be a plane domain, let meet every connected component of , and let be holomorphic. Then is Runge-approximable on with poles in .
Facts & Assumptions
Given: A plane domain , a pole set meeting every component of , and a holomorphic function on .
Every compact set inside 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).
Runge approximation on one compact set holds once the pole set meets every component of its complement (Runge approximation with a prescribed pole set).
Local-uniform approximation on a plane domain means uniform approximation on each compact set in an exhaustion (Runge approximation on a plane domain).
Proof
Choose an increasing exhaustion of compact subsets of with and . By recursively applying [L1] and filling every complementary component of the chosen Jordan neighbourhood that lies entirely in , we may also require that every connected component of meets .
Apply [L2] to each with tolerance . This gives a rational function with poles in and
Fix a compact set . Choose with . Then for every one has , so step 2.1 gives . Hence uniformly on . Since was arbitrary, [L3] gives local-uniform convergence on .
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 .
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 .
The Mittag-Leffler expansion of pi cotangent
Statement
For every ,
where the series converges locally uniformly on .
Facts & Assumptions
Given: The integer pole set and the cotangent function.
The complex sine and cosine are defined by the complex exponential, so their standard formulas are available by direct algebra (Complex sine, cosine, hyperbolic sine, and hyperbolic cosine from the complex exponential).
The zeros of are exactly the integers, and , so is meromorphic with simple residue- poles at the integers (Tangent, cotangent, secant, and cosecant on their exact natural domains, Complex sine, cosine, hyperbolic sine, and hyperbolic cosine are entire with their standard derivatives, The zeros of complex sine are the integer multiples of pi, and the zeros of complex cosine are the odd half-integer multiples of pi).
The residue theorem evaluates contour integrals by enclosed residues. (The residue theorem for a null-homologous cycle)
Proof
Fix . For large enough that , let be the positively oriented rectangle with [L2, L3, given, algebra] vertices and set By [L2], the poles of inside are the integers with and the points . The residue at an integer is , while the residues at and sum to Therefore [L3] gives
On the vertical sides of , write . [L1, step 1.1, algebra] and by [L1], so . On the horizontal sides, , and [L1] gives so . Also on , hence . Thus on , and since the boundary length is , one gets as .
Letting in step 1.1 and using step 2.1 yields [step 1.1, step 2.1, algebra] Multiplying by gives On every compact subset of , the last series is bounded termwise by for all large , so it converges locally uniformly there. This is exactly the claimed expansion.
The partial-fraction expansion of pi-squared cosecant-squared
Statement
For every ,
with locally uniform convergence on .
Facts & Assumptions
Given: The cotangent expansion on .
Locally uniform convergence of holomorphic partial sums forces local-uniform convergence of their derivatives to the derivative of the limit (Locally uniform limits of holomorphic functions are holomorphic and their derivatives converge locally uniformly).
Proof
Let By [L1], the holomorphic functions converge locally uniformly on to . On any compact set , the derivatives satisfy and this derivative series converges uniformly on because its terms are there. Therefore [L3] identifies the derivative of the limit with the displayed series on .
Differentiating [L1] gives by [L2]. Multiplying by yields the claimed formula.
Every discrete effective divisor on a plane domain is the zero divisor of a holomorphic function
Statement
Let be a plane domain, and let be discrete with multiplicities . Then there is a holomorphic function on whose zero at each has order exactly and which has no other zeros.
Facts & Assumptions
Given: A plane domain and a discrete effective divisor on .
The elementary factor has its only zero at (Weierstrass elementary factors).
A normally convergent product of holomorphic factors is holomorphic and has exactly the zeros contributed by its factors (Normally convergent products define holomorphic functions with the expected zeros).
If and is a discrete sequence of nonzero complex numbers, then a product is entire and has exactly the order- zero at and the listed nonzero zeros with multiplicity (Weierstrass product theorem on the complex plane).
Proof
List the points of with each repeated times. If the list is finite, the corresponding finite polynomial works (with for the empty list). If the list is infinite and , let be the multiplicity of and enumerate the remaining nonzero terms as . Fact [L4] applied to and gives the required entire function. Thus assume . Define Split the repeated list into , consisting of the terms in , and , consisting of the remaining terms.
For each , choose with . If is infinite, then : otherwise a subsequence stays a fixed positive distance from the boundary, while the defining inequality for keeps that subsequence bounded, producing a limit point in . Define Each is holomorphic on and, by [L1], has its only zero at .
If is infinite, then . Indeed, a bounded subsequence would have a limit point; discreteness excludes a limit in , while gives which excludes a boundary limit. Let be the multiplicity of in this list and enumerate its nonzero terms as . Then , so [L4] gives an entire function whose zeros, with repetition, are exactly the . If the list is finite, take the corresponding finite polynomial, and if it is empty, take .
Fix a compact set and put . For all sufficiently large , Hence [L2] gives after increasing the starting index if necessary. Thus is normally convergent on , and [L3] gives a holomorphic function whose zeros, with repetition, are exactly the .
The product is holomorphic on . Steps 3.1 and 2.2 show that its zeros are exactly the original points , and repetition in the list gives each zero order .
Every meromorphic function on a plane domain is a quotient of holomorphic functions
Statement
Every meromorphic function on a plane domain is a quotient of holomorphic functions.
Facts & Assumptions
Given: A meromorphic function on a plane domain .
A meromorphic function is holomorphic away from a discrete pole set (Meromorphic functions on a plane domain).
Every discrete effective divisor on a plane domain is the zero divisor of a holomorphic function (Every discrete effective divisor on a plane domain is the zero divisor of a holomorphic function).
A locally bounded punctured singularity is removable (Characterizations of removable singularities).
Proof
Let be the pole set of , with multiplicities equal to pole orders. By [L2], choose a holomorphic function on whose zero divisor is exactly .
On , define . Near a pole , the zero of has exactly the same order as the pole of , so is locally bounded on a punctured neighbourhood of . By [L3], extends holomorphically across every point of .
Away from , one has . Since both sides are meromorphic and agree on the dense open set , this quotient represents on all of .
Meromorphic functions on a connected plane domain form a field
Statement
Let be a connected plane domain. Then the meromorphic functions on form a field under pointwise addition and multiplication.
Facts & Assumptions
Given: A connected plane domain .
Every meromorphic function on is a quotient of holomorphic functions with (Every meromorphic function on a plane domain is a quotient of holomorphic functions).
Proof
Sums and products of meromorphic functions are meromorphic by the pointwise formulas on the common holomorphic locus.
Let be a nonzero meromorphic function. By [L1], write with holomorphic and . Since is connected and , one also has . On the set where , , which is meromorphic; at a zero of this quotient has at worst a pole. Hence is meromorphic on .
Therefore every nonzero meromorphic function has a multiplicative inverse, and together with step 1.1 this makes the meromorphic functions a field.
Choice bookkeeping for Runge and Mittag-Leffler
Remark
The proofs on this page separate two kinds of choice.
First, the compact-set Runge theorem is finitary once the pole representatives are named: the enclosing cycle is a finite polygonal chain, the Riemann sums use finite sampling, and pole pushing moves finitely many poles along finitely many disc chains.
Second, the domain versions need an exhaustion and one representative in each component of . The exhaustion can be chosen canonically, but the complementary representatives are genuine extra data unless the domain already comes with a distinguished choice, for example when the complement is connected and is the pole set. The local proofs therefore stay within ordinary finitary reasoning, while the global statements record exactly where the component-by-component bookkeeping enters.
5 · Examples, counterexamples and false statements
None yet.
Sources
- J. Lebl, Guide to Cultivating Complex Analysis, §9.4
- M. Weber, Complex Analysis, §3.3
- J. Lebl, Guide to Cultivating Complex Analysis, §9.2
- M. Weber, Complex Analysis, §4.4
- J. Lebl, Guide to Cultivating Complex Analysis, §9.2 before Lemma 9.2.2
- M. Weber, Complex Analysis, §4.4 before Lemma 4.4.4
- M. Weber, Complex Analysis, Lemma 4.4.2
- J. Lebl, Guide to Cultivating Complex Analysis, Lemma 9.2.1 setup
- J. Lebl, Guide to Cultivating Complex Analysis, Lemma 9.2.1
- M. Weber, Complex Analysis, Proposition 4.4.1
- J. Lebl, Guide to Cultivating Complex Analysis, Lemma 9.2.2
- M. Weber, Complex Analysis, Lemma 4.4.4
- J. Lebl, Guide to Cultivating Complex Analysis, Theorem 9.2.3
- M. Weber, Complex Analysis, Theorem 4.4.3
- J. Lebl, Guide to Cultivating Complex Analysis, §9.1 and Corollary 9.2.6
- M. Weber, Complex Analysis, Corollary 4.4.5
- J. Lebl, Guide to Cultivating Complex Analysis, Lemma 9.2.5 and Corollary 9.2.6
- M. Weber, Complex Analysis, Theorem 4.4.6
- J. Lebl, Guide to Cultivating Complex Analysis, Corollary 9.2.6
- M. Weber, Complex Analysis, Theorem 3.3.2
- J. Lebl, Guide to Cultivating Complex Analysis, Theorem 9.4.1
- M. Weber, Complex Analysis, Theorem 3.3.2 and Runge Theory
- M. Weber, Complex Analysis, Example 3.3.1
- M. Weber, Complex Analysis, §3.3 and §4.4
- J. Lebl, Guide to Cultivating Complex Analysis, §9.2 and §9.4