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 pseudoconvexity yields a continuous plurisubharmonic exhaustion
Statement
Let be a domain. If is Hartogs pseudoconvex, that is, if is plurisubharmonic on , then admits a continuous plurisubharmonic exhaustion function.
Facts & Assumptions
Given: A domain .
Hartogs pseudoconvexity means exactly that is plurisubharmonic, while a continuous plurisubharmonic exhaustion is defined by compact sublevel sets (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).
Finite maxima preserve plurisubharmonicity (Basic stability operations for plurisubharmonic functions).
With the canonical indices , the squared norm has Levi matrix equal to the identity (reindexing the Levi Definition), so it is plurisubharmonic (The Levi form and strict plurisubharmonicity, The C^2 Levi criterion for plurisubharmonicity).
Canonical complex coordinates are indexed by , and their squared norm is ; under the real coordinate identification, closed bounded subsets are compact. (Complex -space and its real coordinate dictionary)
The equal-radius polydisc boundary function is the sup-norm distance to the complement. For a proper domain it is finite and positive at every point. (The equal-radius polydisc boundary function)
Proof
Write , with when as specified in [L1], and assume is plurisubharmonic. The function is plurisubharmonic by [L3]. For a proper domain, the distance function is positive and continuous on by [L5]: the triangle inequality makes distance to its nonempty complement -Lipschitz. Thus is continuous in that case, and the whole-space convention is continuous as well. Therefore [L2] makes a continuous plurisubharmonic function.
For , the sublevel is empty since . For , it is closed in by continuity and lies in , so it is bounded. If , it is closed in the whole space and hence compact by [L4]. For a proper domain, every also satisfies . If a sequence from converges in to , the -Lipschitz distance-to-complement function gives distance at least at , so ; continuity of then puts . Thus is closed in the whole space, bounded and contained in , hence compact by [L4]. All sublevels are compact, so [L1] gives the promised continuous plurisubharmonic exhaustion.
Depends on
Used by
Dependency tree · two levels
25 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.5.6 (standard reference, not scraped)
- Harold P. Boas, Lecture Notes on Several Complex Variables, Theorem 8 (standard reference, not scraped)