Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-28
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 ΩCm, the following are equivalent.

  1. Ω is a domain of holomorphy.
  2. For every compact KΩ, δΩ(K^Ω)=δΩ(K).
  3. Ω is holomorphically convex.

Facts & Assumptions

Given: A domain ΩCm.

[L1]

On a domain of holomorphy, compact hulls preserve the boundary-radius function exactly (Cartan-Thullen boundary-radius theorem).

[L2]

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).

[L3]

A domain of holomorphy is defined by the failure of every common simultaneous extension pair (Holomorphic extension and domains of holomorphy in several variables).

[L4]

Every open connected subset of Euclidean space is polygonally connected (For an open subset of Rn, connectedness, path-connectedness and polygonal connectedness are equivalent).

[L5]

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

technique · direct
1.1

Property 1 implies property 2 by [L1].

L1
1.2

Assume property 3. If Ω=Cm, property 1 holds directly from [L3]. Otherwise fix pΩ and a connected open set CΩ with pC. Let (Dn) be an increasing compact exhaustion of Ω. Construct increasing holomorphically convex compact sets Kn and points pnp recursively. Start with K1:=D1^Ω. Once KnΩ is chosen, choose pnCKn with pnp<1/n, and put Kn+1:=KnDn+1{pn}^Ω. Property 3 and idempotence of hulls make each Kn compactly contained in Ω, and pnKj whenever j>n.

L2L3givenchooseconstruct
2.1

Since pnK^nΩ=Kn, choose gnO(Ω) with gn(pn)>supKngn. Taking a sufficiently large positive power makes the ratio of these two quantities arbitrarily large; scaling that power then gives fnO(Ω) such that supKnfn<2nandfn(pn)>n+1+j<nfj(pn). Every compact subset of Ω lies in some KN, so nfn converges uniformly on compact subsets to a holomorphic function f. Moreover, pnKj for j>n, so j>nfj(pn)<j>n2j<1. The reverse triangle inequality and the second displayed bound give f(pn)>n.

step 1.2L2algebrachoose
2.2

Assume property 2, and let KΩ be compact. By [L2], the hull K^Ω is closed in Ω and coordinate-bounded. Property 2 gives δΩ(K^Ω)=δΩ(K)>0, so every point of K^Ω carries a positive-radius polydisc contained in Ω. Hence every Euclidean limit point of K^Ω still lies in Ω, and the closedness from [L2] makes K^Ω closed in Cm. Being closed and bounded in finite-dimensional Euclidean space, it is compact; the positive boundary-radius lower bound keeps it away from Ω. Thus K^ΩΩ, so property 3 holds.

L2step 1.1algebra
3.1

Suppose toward a contradiction that domains U1,U2 witness failure of property 1 as in [L3]. Choose aU1 and bU2Ω. By [L4], join them by a path in U2, and let p be its first point on Ω. The part of the path before p lies in the connected component C of ΩU2 containing U1, so pC. Apply steps 1.2 and 2.1 with this p and C, obtaining fO(Ω) and pnC with pnp and f(pn)>n. By the assumed simultaneous-extension property, f has an extension FO(U2) agreeing with f on U1. The identity theorem [L5] gives F=f on C, but continuity makes F bounded near pU2, contradicting F(pn)>n. Thus property 3 implies property 1, and the three properties are equivalent.

L3L4L5step 1.2step 2.1assume-contradischarge-contradiction

Depends on

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