Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck pass
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 Ω⊆Cm be a domain. If Ω is Hartogs pseudoconvex, that is, if −log⁡δΩ is plurisubharmonic on Ω, then Ω admits a continuous plurisubharmonic exhaustion function.

Facts & Assumptions

Given: A domain Ω⊆Cm.

[L1]

Hartogs pseudoconvexity means exactly that −log⁡δΩ is plurisubharmonic, while a continuous plurisubharmonic exhaustion is defined by compact sublevel sets (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).

[L2]

Finite maxima preserve plurisubharmonicity (Basic stability operations for plurisubharmonic functions).

[L3]

With the canonical indices j<m, the squared norm q(z)=∑j<m∣zj∣2 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).

[L4]

Canonical complex coordinates are indexed by j<m, and their squared norm is ∑j<m∣zj∣2; under the real coordinate identification, closed bounded subsets are compact. (Complex m-space and its real coordinate dictionary)

[L5]

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

technique · direct
1.1L1L2L3L4L5given

Write b(z)=−log⁡δΩ(z), with b≡0 when Ω=Cm as specified in [L1], and assume b is plurisubharmonic. The function q(z)=∑j<m∣zj∣2 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 1-Lipschitz. Thus b is continuous in that case, and the whole-space convention is continuous as well. Therefore [L2] makes u(z):=max⁡{b(z),q(z)} a continuous plurisubharmonic function.

2.1L1L4L5step 1.1givenalgebra∎

For c<0, the sublevel Kc:={z∈Ω:u(z)≤c} is empty since q≥0. For c≥0, it is closed in Ω by continuity and lies in {q≤c}, so it is bounded. If Ω=Cm, it is closed in the whole space and hence compact by [L4]. For a proper domain, every z∈Kc also satisfies δΩ(z)≥e−c. If a sequence from Kc converges in Cm to a, the 1-Lipschitz distance-to-complement function gives distance at least e−c at a, so a∈Ω; continuity of u then puts a∈Kc. Thus Kc 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