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.
An isolated puncture is removable in complex dimension at least two
Statement
Let , let be a domain, let , and let be holomorphic. Then there exists a unique holomorphic such that on .
Facts & Assumptions
Given: A domain with , a point , and a holomorphic function .
Every point of an open subset of has a polydisc neighborhood inside that open set (Balls, polydiscs and the distinguished boundary in ).
A contour integral of a jointly continuous integrand that is holomorphic in the parameter variable defines a holomorphic function of that parameter (A contour integral of a jointly continuous, parameter-holomorphic integrand is holomorphic).
The one-variable Cauchy integral formula recovers a holomorphic function on a disc from any interior circle (Cauchy's integral formula on a circle compactly contained in a disc of holomorphy).
A holomorphic function on a connected open set is determined by its values on a nonempty open subset (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).
A separately holomorphic function that is locally bounded is jointly holomorphic (Locally bounded and separately holomorphic implies holomorphic).
Proof
By [L1], choose radii and with . For with and , define When and , the point lies in , so the integrand is well defined and continuous there.
Fix all variables except one. If the free variable is , the Cauchy kernel makes holomorphic on . If the free variable is one coordinate of , then [L2] applies to that single complex parameter. So is separately holomorphic on . The same integral formula gives local bounds on compact subsets, so [L5] upgrades to a jointly holomorphic function there.
If , then the slice is holomorphic on the full disc , because the deleted point does not lie on that slice. Hence [L3] gives for every .
The set is a nonempty open subset of , and step 2.2 shows that and agree there. Both are holomorphic on the connected punctured polydisc , so [L4] forces on all of .
Thus is a holomorphic extension of across on the neighborhood . Repeating the same construction at each puncture point gives a local extension, and uniqueness on overlaps again follows from [L4]. Therefore the local extensions glue to a unique holomorphic function on all of .
Depends on
- Balls, polydiscs and the distinguished boundary in $\mathbb{C}^m$
- A contour integral of a jointly continuous, parameter-holomorphic integrand is holomorphic
- Cauchy's integral formula on a circle compactly contained in a disc of holomorphy
- A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically
- Locally bounded and separately holomorphic implies holomorphic
Used by
- Holomorphic functions of several variables have no isolated singularities Corollary
- A holomorphic function on the punctured bidisc extends across the origin Example
- The bidisc minus the origin is not a domain of holomorphy Example
- FALSE: every holomorphic function on a punctured several-variable domain is unbounded near the puncture False statement
Dependency tree · two levels
42 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
- J. Lebl, Tasty Bits of Several Complex Variables, Theorem 1.6.1 (standard reference, not scraped)