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.
Cartan-Thullen theorem
Statement
For a domain , the following are equivalent.
- is a domain of holomorphy.
- For every compact ,
- is holomorphically convex.
Facts & Assumptions
Given: A domain .
On a domain of holomorphy, compact hulls preserve the boundary-radius function exactly (Cartan-Thullen boundary-radius theorem).
Hulls contain the original compact set, are closed in , and are coordinate-bounded for compact inputs (Basic properties of the holomorphic hull, Holomorphic hulls and holomorphic convexity).
A domain of holomorphy is defined by the failure of every common simultaneous extension pair (Holomorphic extension and domains of holomorphy in several variables).
Every open connected subset of Euclidean space is polygonally connected (For an open subset of , connectedness, path-connectedness and polygonal connectedness are equivalent).
Holomorphic functions on a connected domain that agree on a nonempty open set agree everywhere (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).
Proof
Property 1 implies property 2 by [L1].
Assume property 3. If , property 1 holds directly from [L3]. Otherwise fix and a connected open set with . Let be an increasing compact exhaustion of . Construct increasing holomorphically convex compact sets and points recursively. Start with . Once is chosen, choose with , and put Property 3 and idempotence of hulls make each compactly contained in , and whenever .
Since , choose with . Taking a sufficiently large positive power makes the ratio of these two quantities arbitrarily large; scaling that power then gives such that Every compact subset of lies in some , so converges uniformly on compact subsets to a holomorphic function . Moreover, for , so The reverse triangle inequality and the second displayed bound give .
Assume property 2, and let be compact. By [L2], the hull is closed in and coordinate-bounded. Property 2 gives , so every point of carries a positive-radius polydisc contained in . Hence every Euclidean limit point of still lies in , and the closedness from [L2] makes closed in . Being closed and bounded in finite-dimensional Euclidean space, it is compact; the positive boundary-radius lower bound keeps it away from . Thus , so property 3 holds.
Suppose toward a contradiction that domains witness failure of property 1 as in [L3]. Choose and . By [L4], join them by a path in , and let be its first point on . The part of the path before lies in the connected component of containing , so . Apply steps 1.2 and 2.1 with this and , obtaining and with and . By the assumed simultaneous-extension property, has an extension agreeing with on . The identity theorem [L5] gives on , but continuity makes bounded near , contradicting . Thus property 3 implies property 1, and the three properties are equivalent.
Depends on
- Holomorphic extension and domains of holomorphy in several variables
- Holomorphic hulls and holomorphic convexity
- Basic properties of the holomorphic hull
- Cartan-Thullen boundary-radius theorem
- For an open subset of $\mathbb{R}^n$, connectedness, path-connectedness and polygonal connectedness are equivalent
- A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically
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
- Jiří Lebl, Tasty Bits of Several Complex Variables, Theorem 2.6.3 (standard reference, not scraped)
- Harold P. Boas, Lecture Notes on Several Complex Variables, Theorems 5 and 6 (standard reference, not scraped)