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.1

Choose radii Rn so that AD(0,Rn)= and AD(0,Rn) is finite for every n. [given, L1, choose] Put S1:=AD(0,R1),Sn:=A(D(0,Rn)D(0,Rn1))(n2). Then each Sn is finite and A=n1Sn. For n2, the finite sum fn(z):=akSnpk(z) is holomorphic on a neighbourhood of D(0,Rn1), because every pole it carries lies outside that disc. Set likewise f1(z):=akS1pk(z).

givenL1choose
2.1

By [L2], for each n2 choose a polynomial qn such that [L2, step 1.1, construct] supzRn1fn(z)qn(z)<2n. Put g1:=f1 and gn:=fnqn for n2. Then every gn is meromorphic on C, has the same principal parts as the finitely many pk with akSn, and is holomorphic on D(0,Rn1).

L2step 1.1construct
3.1

Fix a compact set KCA. Choose with [step 2.1, choose, algebra, discharge-construct] KD(0,R). For every n+1, one has KD(0,Rn1), so step 2.1 gives supKgn2n. Hence n1gn converges uniformly on K. Near any point akS, all terms except g are holomorphic, so the sum f:=n1gn is meromorphic on C and has principal part pk at ak.

step 2.1choosealgebradischarge-construct

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