Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-30
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 A={a1,a2,… }⊆C be a discrete set, listed so that ∣an∣→∞, and let pn be a prescribed principal part at an for each n. Then there is a meromorphic function f on C whose principal part at an is pn for every n.

Facts & Assumptions

Given: A discrete set A={an} with ∣an∣→∞ and prescribed principal parts pn.

[L1]

A prescribed principal part is a finite negative Laurent polynomial at the chosen point (The principal part at an isolated singularity).

[L2]

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

technique · constructive
1.1givenL1choose

Choose radii Rn↑∞ so that A∩∂D(0,Rn)=∅ and A∩D‾(0,Rn) is finite for every n. [given, L1, choose] Put S1:=A∩D‾(0,R1),Sn:=A∩(D‾(0,Rn)∖D‾(0,Rn−1))(n≥2). Then each Sn is finite and A=⨆n≥1Sn. For n≥2, the finite sum fn(z):=∑ak∈Snpk(z) is holomorphic on a neighbourhood of D‾(0,Rn−1), because every pole it carries lies outside that disc. Set likewise f1(z):=∑ak∈S1pk(z).

2.1L2step 1.1construct

By [L2], for each n≥2 choose a polynomial qn such that [L2, step 1.1, construct] sup⁡∣z∣≤Rn−1∣fn(z)−qn(z)∣<2−n. Put g1:=f1 and gn:=fn−qn for n≥2. Then every gn is meromorphic on C, has the same principal parts as the finitely many pk with ak∈Sn, and is holomorphic on D‾(0,Rn−1).

3.1step 2.1choosealgebradischarge-construct∎

Fix a compact set K⊆C∖A. Choose ℓ with [step 2.1, choose, algebra, discharge-construct] K⊆D‾(0,Rℓ). For every n≥ℓ+1, one has K⊆D‾(0,Rn−1), so step 2.1 gives sup⁡K∣gn∣≤2−n. Hence ∑n≥1gn converges uniformly on K. Near any point ak∈Sℓ, all terms except gℓ are holomorphic, so the sum f:=∑n≥1gn is meromorphic on C and has principal part pk at ak.

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