Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26
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.

Characterizations of removable singularities

Statement

Let f be holomorphic on a punctured disc 0<∣z−a∣<R. The following are equivalent:

  1. a is a removable singularity of f (Isolated singularities: removable, poles, and essential singularities);
  2. the principal part of the Laurent expansion of f at a is 0 (The principal part of a Laurent series);
  3. f is bounded on some punctured neighbourhood of a;
  4. f has a finite limit as z→a;
  5. (z−a)f(z)→0 as z→a.

When these conditions hold, the holomorphic extension satisfies F(a)=lim⁡z→af(z).

Facts & Assumptions

Given: A function f holomorphic on 0<∣z−a∣<R and its Laurent expansion f(z)=∑n∈Zcn(z−a)n there.

[L1]

Every holomorphic function on a punctured disc has a Laurent expansion there, its coefficients are unique, and the regular part extends holomorphically across the centre (Laurent expansion on an annulus, Laurent coefficients are given by contour integrals and are unique, Laurent series split into regular and principal parts).

[L2]

A removable singularity is exactly one admitting a holomorphic extension across the centre (Isolated singularities: removable, poles, and essential singularities).

[L3]

Proof

technique · direct
1.1L2L3

If a is removable, let F be a holomorphic extension to ∣z−a∣<ε; by [L3], F is continuous at a, so F is bounded on some smaller disc, and hence f is bounded on the corresponding punctured disc.

1.2givenalgebra

If f has a finite limit at a, then f is bounded on some punctured neighbourhood of a.

1.3L1assume-hypalgebra

Suppose ∣f(z)∣≤M whenever 0<∣z−a∣<ε. For m≥1 and 0<ρ<ε, the coefficient formula gives ∣c−m∣≤12π∫∣ζ−a∣=ρ∣f(ζ)∣ ∣ζ−a∣m−1∣dζ∣≤Mρm.

1.4L1L2

If the principal part is 0, then f(z)=∑n≥0cn(z−a)n on the punctured disc, and [L1] makes this regular part holomorphic on ∣z−a∣<R; defining F(a)=c0 therefore extends f holomorphically across a, so the singularity is removable.

2.1step 1.3

Since step 1.3 holds for every sufficiently small ρ>0, letting ρ→0 gives c−m=0 for every m≥1; so the principal part is 0.

2.2step 1.4L3

The extension from step 1.4 is continuous at a by [L3], so f(z)→F(a)=c0 and, multiplying by z−a, one gets (z−a)f(z)→0.

3.1step 1.3step 2.1L1

Suppose (z−a)f(z)→0, and put g(z):=(z−a)f(z) on the punctured disc. Then g is holomorphic there and bounded near a, so the argument of steps 1.3 and 2.1 applied to the Laurent expansion g(z)=∑n∈Zcn(z−a)n+1 gives c−m=0 for every m≥2.

4.1step 2.2step 3.1L1

With the coefficients from step 3.1 gone, g(z)=c−1+∑n≥0cn(z−a)n+1, and [L1] makes the tail a holomorphic function vanishing at a; the hypothesis g(z)→0 therefore forces c−1=0. So the whole principal part of f is 0.

5.1step 1.1step 1.2step 2.1step 1.4step 2.2step 4.1∎

Step 1.1 proves 1⇒3, step 1.2 proves 4⇒3, steps 1.3 and 2.1 prove 3⇒2, step 1.4 proves 2⇒1, step 2.2 proves 2⇒4 and 2⇒5, and steps 3.1 and 4.1 prove 5⇒2; therefore all five conditions are equivalent, and the extension value is the finite limit from step 2.2.

Depends on

Used by

Dependency tree · two levels

19 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