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.

Domains of holomorphy are Hartogs pseudoconvex

Statement

Every domain of holomorphy in Cm is Hartogs pseudoconvex.

Facts & Assumptions

Given: A domain of holomorphy ΩCm.

[L1]

Domains of holomorphy satisfy the continuity principle for continuous families of analytic discs (Continuity principle for domains of holomorphy).

[L2]

Hartogs pseudoconvexity means that logδΩ is plurisubharmonic (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).

[L3]

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

[L4]

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

[L5]

Plane subharmonicity is the upper-semicontinuous disc-submean condition (Subharmonic functions on plane domains).

Proof

technique · direct
1.1

If Ω=Cm, it is Hartogs pseudoconvex by the whole-space convention in [L2]. Assume henceforth that Ω is proper. Fix an affine map λz0+λw0 from the closed unit disc into Ω, and put u(λ):=logδΩ(z0+λw0). By [L3], u 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 z=z1 on the circle. Given ε>0, [L4] therefore gives a complex trigonometric polynomial within ε of the real function u; taking its real part gives a real trigonometric polynomial q with qu<ε. Write q(eit)=Rep(eit) for a holomorphic polynomial p, and replace p by p+ε. Then u(λ)<Rep(λ)u(λ)+2ε(λ=1).

L2L3L4givenchooseconstruct
2.1

For ηCm with maxjηj<1 and t[0,1], define Φtη(λ):=z0+λw0+tep(λ)η. On λ=1, the perturbation has sup norm strictly less than δΩ(z0+λw0), so each boundary circle Φtη(D) lies in Ω. The initial disc at t=0 also lies in Ω, so [L1] applied to the family tΦtη gives Φ1η(D)Ω. Since this holds for every η in the unit polydisc, the whole equal-radius polydisc of radius eRep(λ) around z0+λw0 lies in Ω for every λ<1. Thus logδΩ(z0+λw0)Rep(λ)(λ<1).

L1step 1.1given
3.1

Evaluating step 2.1 at 0 and averaging the boundary values of the real part of the polynomial p gives u(0)Rep(0)=12π02πRep(eit)dt12π02πu(eit)dt+2ε. Letting ε0 gives the submean inequality. Because the affine closed disc was arbitrary and u is continuous, [L5] makes every affine-line restriction subharmonic. By [L2], logδΩ is plurisubharmonic, so Ω is Hartogs pseudoconvex.

L2L5step 1.1step 2.1algebra

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