Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 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 with a prescribed pole set

Statement

Let KC be compact, let U be an open neighbourhood of K, let f:UC be holomorphic, and let PC^K be a Runge pole set for K. Then for every ε>0 there is a rational function r with poles only in P such that

supzKf(z)r(z)<ε.

Facts & Assumptions

Given: A compact set K, a holomorphic function f on a neighbourhood of K, a Runge pole set P, and a tolerance ε>0.

[L1]

The Cauchy integral over a suitable enclosing cycle can be approximated uniformly on K by rational functions with poles on that cycle (Riemann sums of the Cauchy integral give rational approximation).

[L2]

A Runge pole set meets every complementary component of C^K (Runge pole sets for rational approximation on a compact set).

[L3]

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

technique · direct
1.1

By [L1], choose a rational function r0(z)=ν=1Ncν/(zaν) whose poles aν lie in C^K and such that supzKf(z)r0(z)<ε/2.

givenL1construct
2.1

If N=0, then r0 already has no finite poles, so its poles are contained in P and step 1.1 already proves the theorem. Assume from now on that N1.

step 1.1cases
3.1

For each pole aν, let Cν be the connected component of C^K containing it. By [L2], choose pνPCν. Applying [L3] to the function cν/(zaν) inside Cν, choose a rational function sν with poles only at pν and supzKsν(z)cνzaν<ε2N.

L2L3step 1.1step 2.1choose
4.1

Put r=ν=1Nsν. Then every pole of r lies in P, and the triangle inequality together with steps 1.1 and 3.1 gives supzKf(z)r(z)supzKf(z)r0(z)+ν=1NsupzKsν(z)cνzaν<ε.

step 1.1step 2.1step 3.1algebra

Depends on

Used by

Dependency tree · two levels

9 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