TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-09-29

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.

Hartogs extension across a connected compact hole with a finite shell cover

Statement

Let $m \geq 2$ , let $Ω \subseteq C^{m}$ be a domain, and let $K ⋐ Ω$ be compact with $Ω ∖ K$ connected. Assume that $K$ admits a finite shell cover: there are open polydiscs $P_{1}, \dots, P_{N} \subseteq Ω$ covering $K$ such that

for each $j$ , the punctured set $P_{j} \cap (Ω ∖ K)$ is connected and contains a coordinate shell of the type treated in Hartogs figures give local extension across polydisc shells whose hull is $P_{j}$ ;
after reordering, every connected component of $P_{j} \cap ((Ω ∖ K) \cup P_{1} \cup \dots \cup P_{j - 1})$ has nonempty intersection with $Ω ∖ K$ for every $j \geq 2$ .

Then every holomorphic function on $Ω ∖ K$ extends uniquely to a holomorphic function on $Ω$ .

Facts & Assumptions

Given: A domain $Ω$ , a compact set $K ⋐ Ω$ , connected complement $Ω ∖ K$ , and a finite shell cover $P_{1}, \dots, P_{N}$ as in the Statement.

[L1]

Each coordinate shell extends holomorphically to its hull polydisc (Hartogs figures give local extension across polydisc shells).

[L2]

Local extension neighborhoods propagate along finite chains and glue uniquely (Local Hartogs extensions propagate along chains and glue uniquely).

[L3]

Holomorphic functions on connected open sets are determined by agreement on one nonempty open subset (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).

[L4]

Holomorphic extension is the overlap-agreement notion fixed on this page (Holomorphic extension and domains of holomorphy in several variables).

Proof

technique · direct

1.1L1L2L3given

Put $G : = Ω ∖ K$ and let $f \in O (G)$ . For each $j$ , choose the shell $S_{j} \subseteq P_{j} \cap G$ from assumption 1. Given any $g \in O (P_{j} \cap G)$ , [L1] extends $g ∣_{S_{j}}$ to a holomorphic $E_{g}$ on the hull $P_{j}$ . The functions $E_{g}$ and $g$ agree on the nonempty open set $S_{j}$ inside the connected open set $P_{j} \cap G$ ; by [L3] they agree on all of $P_{j} \cap G$ . This is the full-overlap local extension property required by [L2], for every $g$ , not only for $f$ . Each $P_{j} \cap G$ is nonempty because it contains $S_{j}$ , and assumption 2 is exactly the componentwise overlap condition of [L2]. Thus $(P_{j})$ satisfies every hypothesis of [L2].

2.1step 1.1L2

Applying [L2] gives a holomorphic extension of $f$ from $G$ to $G \cup P_{1} \cup \dots \cup P_{N}$ . Because the polydiscs cover $K$ , this union is all of $Ω$ .

3.1L3L4step 2.1∎

Uniqueness follows from [L3]: two extensions to $Ω$ agree on the nonempty open subset $Ω ∖ K$ , so they agree on all of the connected domain $Ω$ . The overlap language in [L4] is exactly the one used in step 1.1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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 4.3.1 (standard reference, not scraped)