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 plane domains

Statement

Let ΩC be a plane domain, let AΩ be a discrete set, and for each aA let pa be a prescribed principal part at a. Then there is a meromorphic function on Ω whose principal part at each aA is pa.

Facts & Assumptions

Given: A plane domain Ω, a discrete set AΩ, and a prescribed principal part pa at each aA.

[L1]

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

[L2]

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

[L3]

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

Proof

technique · constructive
1.1

Choose an increasing compact exhaustion C1C2 of Ω with CnCn+1 and nCn=Ω. [given, L1, L3, construct] Recursively apply [L1] to choose compact Jordan neighbourhoods of the Cn and then fill every complementary component lying entirely in Ω. This gives an increasing exhaustion K1K2 of compact subsets of Ω such that every connected component of C^Kn meets C^Ω. Because A is discrete, each set An:=A(KnKn1)(K0:=) is finite. Let fn(z):=aAnpa(z). Then fn is meromorphic on Ω and holomorphic on a neighbourhood of Kn1.

givenL1L3construct
2.1

Fix a set PC^Ω meeting every connected component of C^Ω. [L2, step 1.1, choose] Step 1.1 makes P meet every connected component of C^Kn1 as well. Put r1:=0 and h1:=f1. For each n2, apply [L2] to fn on a neighbourhood of Kn1 and choose a rational function rn with poles in P such that supKn1fnrn<2n. Then hn:=fnrn is meromorphic on Ω, has the same principal parts as fn on An, and is uniformly small on Kn1.

L2step 1.1choose
3.1

For a compact set KΩA, choose N with [step 2.1, algebra, discharge-construct] KKN1. Then for every nN, step 2.1 gives supKhn2n. Therefore nhn converges uniformly on K. Only finitely many layers An meet a given compact set, so f:=n1hn is meromorphic on Ω, and its principal part at each aAn is exactly pa.

step 2.1algebradischarge-construct

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