LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pendingjudge pass (gpt-6-luna)

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.

Laurent decomposition of holomorphic functions on the punctured plane

Statement

Let $C^{*} = C ∖ {0}$ . For every holomorphic function $f \in O (C^{*})$ , there are unique entire functions $g, h \in O (C)$ and a unique scalar $a \in C$ such that

f (z) = g (z) + a z^{- 1} + z^{- 2} h (1 / z) (z \in C^{*}) .

Statement references

L. V. Ahlfors, Complex Analysis, Chapter 5 §1.3

Jeremy Orloff, MIT 18.04 Topic 7: Taylor and Laurent Series

Facts & Assumptions

Given: A holomorphic function $f$ on the punctured plane $C^{*} = A (0; 0, + \infty)$ .

[F1]

Every holomorphic function on an annulus has a Laurent series converging uniformly on each compact subannulus (Annuli in the complex plane, Convergent Laurent series on an annulus, Laurent expansion on an annulus).

[F2]

Uniform convergence of continuous contour integrands allows passage of the limit through the complex line integral (A uniformly convergent sequence of continuous integrands on a fixed contour permits passage of the limit through the complex line integral).

[F3]

Locally uniform limits of holomorphic functions on an open subset of $C$ are holomorphic (Locally uniform limits of holomorphic functions are holomorphic, with locally uniform convergence of all derivatives).

Proof

1.1F1F2givenconstruct

By [F1], write $f (z) = \sum_{n \in Z} c_{n} z^{n}$ on $C^{*}$ , with both one-sided series uniformly convergent on every compact subannulus. Fix $R > 0$ and integrate the uniformly convergent series on the positively oriented circle $γ_{R} (t) = R e^{i t}$ after multiplying by $z^{- n - 1}$ . By [F2], termwise integration is valid, and direct parametrization gives $(2 π i)^{- 1} \int_{γ_{R}} z^{k - n - 1} d z = 1$ for $k = n$ and $0$ otherwise. Thus $c_{n} = \frac{1}{2 π i} \int_{γ_{R}} f (z) z^{- n - 1} d z$ for every $n \in Z$ and every $R > 0$ .

2.1step 1.1algebra

Put $M_{R} = \max_{∣ z ∣ = R} ∣ f (z) ∣$ . The coefficient formula in step 1.1 and the circle length $2 π R$ give $∣ c_{n} ∣ \leq M_{R} R^{- n}$ for $n \geq 0$ and $∣ c_{- m} ∣ \leq M_{R} R^{m}$ for $m \geq 1$ .

3.1F3step 2.1construct

Define $g (z) = \sum_{n \geq 0} c_{n} z^{n}$ . For any $S > 0$ , choose $R > S$ ; on $∣ z ∣ \leq S$ the terms satisfy $∣ c_{n} z^{n} ∣ \leq M_{R} (S / R)^{n}$ by step 2.1, so the series converges uniformly there. Its partial sums are polynomials, hence [F3] makes $g$ entire.

3.2F3step 2.1construct

Define $h (w) = \sum_{j \geq 0} c_{- (j + 2)} w^{j}$ . Given $S > 0$ , choose $0 < R < 1 / S$ ; on $∣ w ∣ \leq S$ the terms satisfy $∣ c_{- (j + 2)} w^{j} ∣ \leq M_{R} R^{2} (R S)^{j}$ by step 2.1, so this series also converges uniformly on every closed disk. Its partial sums are polynomials, and [F3] makes $h$ entire.

4.1F1step 3.1step 3.2

On each compact subannulus of $C^{*}$ , the Laurent series of [F1] is the sum of its nonnegative terms, its single $c_{- 1} z^{- 1}$ term, and its terms of degree at most $- 2$ . The first part is $g (z)$ by step 3.1, and the last part is $z^{- 2} h (1 / z)$ by step 3.2. Hence the displayed decomposition holds at every $z \neq 0$ .

5.1step 1.1step 4.1algebra∎

If another pair of entire functions and scalar gave the same decomposition, their Taylor coefficients would give a Laurent expansion of $f$ on $C^{*}$ with the same positive, $- 1$ , and lower negative powers. The contour formula in step 1.1 recovers each Laurent coefficient uniquely; therefore the scalar and all Taylor coefficients of both entire functions agree. The decomposition is unique.

Laurent decomposition of holomorphic functions on the punctured plane

Statement

Statement references

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources