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.

Runge approximation on plane domains

Statement

Let Ω⊆C be a plane domain, let P⊆C^∖Ω meet every connected component of C^∖Ω, and let f:Ω→C be holomorphic. Then f is Runge-approximable on Ω with poles in P.

Facts & Assumptions

Given: A plane domain Ω, a pole set P meeting every component of C^∖Ω, and a holomorphic function f on Ω.

[L1]

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

[L2]

Runge approximation on one compact set holds once the pole set meets every component of its complement (Runge approximation with a prescribed pole set).

[L3]

Local-uniform approximation on a plane domain means uniform approximation on each compact set in an exhaustion (Runge approximation on a plane domain).

Proof

technique · direct
1.1givenL1construct

Choose an increasing exhaustion K1⊆K2⊆⋯ of compact subsets of Ω with ⋃nKn=Ω and Kn⊆int⁡Kn+1. 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 C^∖Kn meets P.

2.1L2step 1.1choose

Apply [L2] to each Kn with tolerance 2−n. This gives a rational function rn with poles in P and sup⁡z∈Kn∣f(z)−rn(z)∣<2−n.

3.1step 2.1L3algebra∎

Fix a compact set K⊆Ω. Choose N with K⊆KN. Then for every n≥N one has K⊆Kn, so step 2.1 gives sup⁡z∈K∣f(z)−rn(z)∣≤2−n. Hence rn→f uniformly on K. Since K was arbitrary, [L3] gives local-uniform convergence on Ω.

Depends on

Used by

Dependency tree · two levels

15 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