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 poles

Statement

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

  1. a is a pole of f;
  2. the Laurent expansion of f has a finite nonzero principal part;
  3. ∣f(z)∣→∞ as z→a;
  4. 1/f extends holomorphically across a and vanishes there.

If these conditions hold and the principal part is

c−m(z−a)−m+c−(m−1)(z−a)−(m−1)+⋯+c−1(z−a)−1

with c−m≠0, then the pole order is m.

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]

A removable singularity is exactly one whose principal part is zero, and a holomorphic function with a finite limit at a extends across a with that value (Characterizations of removable singularities).

[L2]

A holomorphic function has a zero of finite order m exactly when it factors as (z−a)mg(z) with g holomorphic and g(a)≠0 (The order of a zero is the exponent in its local holomorphic factorization).

[L3]

Reciprocal and product rules hold for holomorphic functions, and a holomorphic function is continuous (Linearity, product, reciprocal, and quotient rules for complex derivatives, Complex differentiability at a point implies continuity there).

[L4]

A pole of order m means that (z−a)mf(z) extends holomorphically across a with a nonzero value there (Isolated singularities: removable, poles, and essential singularities); order 1 is the special case of a simple pole (Simple poles).

[L5]

Every holomorphic function on a punctured disc has a Laurent expansion there, and a removable singularity gives a regular part that extends holomorphically across the centre (Laurent expansion on an annulus, Characterizations of removable singularities, Laurent series split into regular and principal parts).

Proof

technique · direct
1.1L4L5

Suppose a is a pole of order m. Then [L4] gives a holomorphic extension g of (z−a)mf(z) with g(a)≠0. The singularity of g at a is removable, so [L5] writes g(z)=∑n≥0bn(z−a)n near a with b0=g(a)≠0; dividing by (z−a)m gives f(z)=∑n≥0bn(z−a)n−m, whose principal part is finite and nonzero and ends at (z−a)−m.

1.2L1L4

Suppose the principal part is finite and nonzero, and let m be the largest index with c−m≠0. Then g(z):=(z−a)mf(z)=c−m+∑k≥1−mck(z−a)k+m has zero principal part, so [L1] makes g holomorphic at a with g(a)=c−m≠0. Therefore a is a pole of order m by [L4].

1.3L1L3

Suppose ∣f(z)∣→∞ as z→a. Then f is nonzero on some punctured neighbourhood of a, so h:=1/f is holomorphic there by [L3], and h(z)→0. By [L1], h extends holomorphically across a with value 0, proving condition 4.

1.4L2L3L4

Suppose condition 4 holds. By [L2], the extension of 1/f factors as (z−a)mu(z) for some m≥1 and some holomorphic u with u(a)≠0; shrinking the disc if needed, u stays nonzero there, so f(z)=(z−a)−mu(z)−1 and a is a pole of order m by [L3] and [L4].

2.1step 1.1L3

The extension g of step 1.1 is continuous and nonzero at a, so ∣g(z)∣≥δ>0 near a; therefore ∣f(z)∣=∣g(z)∣∣z−a∣−m≥δ∣z−a∣−m→∞.

3.1step 1.1step 2.1step 1.2step 1.3step 1.4∎

Step 1.1 proves 1⇒2, step 2.1 proves 1⇒3, step 1.2 proves 2⇒1, step 1.3 proves 3⇒4, and step 1.4 proves 4⇒1; hence all four conditions are equivalent, and the pole order is the largest negative exponent present in the finite principal part.

Depends on

Used by

Dependency tree · two levels

28 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