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.
Domains of holomorphy are Hartogs pseudoconvex
Statement
Every domain of holomorphy in is Hartogs pseudoconvex.
Facts & Assumptions
Given: A domain of holomorphy .
Domains of holomorphy satisfy the continuity principle for continuous families of analytic discs (Continuity principle for domains of holomorphy).
Hartogs pseudoconvexity means that is plurisubharmonic (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).
The boundary-radius function is the sup-norm distance to the complement, so it is continuous on a proper domain (The equal-radius polydisc boundary function).
Every unital point-separating self-adjoint complex function algebra on a compact Hausdorff space is uniformly dense (Complex Stone–Weierstrass dichotomy for separating self-adjoint algebras; the unital case is dense).
Plane subharmonicity is the upper-semicontinuous disc-submean condition (Subharmonic functions on plane domains).
Proof
If , it is Hartogs pseudoconvex by the whole-space convention in [L2]. Assume henceforth that is proper. Fix an affine map from the closed unit disc into , and put By [L3], is continuous on the closed disc. The trigonometric-polynomial algebra on the unit circle is unital, separates points through the coordinate function, and is self-adjoint because on the circle. Given , [L4] therefore gives a complex trigonometric polynomial within of the real function ; taking its real part gives a real trigonometric polynomial with . Write for a holomorphic polynomial , and replace by . Then
For with and , define On , the perturbation has sup norm strictly less than , so each boundary circle lies in . The initial disc at also lies in , so [L1] applied to the family gives . Since this holds for every in the unit polydisc, the whole equal-radius polydisc of radius around lies in for every . Thus
Evaluating step 2.1 at and averaging the boundary values of the real part of the polynomial gives Letting gives the submean inequality. Because the affine closed disc was arbitrary and is continuous, [L5] makes every affine-line restriction subharmonic. By [L2], is plurisubharmonic, so is Hartogs pseudoconvex.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
17 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, §2.5 (standard reference, not scraped)
- Harold P. Boas, Lecture Notes on Several Complex Variables, Theorem 8 (standard reference, not scraped)