LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27

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.

A weak local subharmonic peak function upgrades to regularity

Statement

Let $Ω \subseteq C$ be a bounded complex domain and let $ζ \in \partial Ω$ . Suppose there are a neighbourhood $U$ of $ζ$ and a subharmonic function $q$ on $Ω \cap U$ such that:

$q (z) < 0$ on $Ω \cap U$ ;
$q (z) \to 0$ as $z \to ζ$ with $z \in Ω$ ;
writing $q^{\partial} (η) : = {lim sup}_{\begin{array}{c} z \to η \\ z \in Ω \cap U \end{array}} q (z) (η \in \overline{Ω \cap U}),$ every compact set $K \subseteq (\overline{Ω \cap U}) ∖ {ζ}$ satisfies $\sup_{η \in K} q^{\partial} (η) < 0$ .

Then $ζ$ is regular for $Ω$ .

Facts & Assumptions

Given: A bounded complex domain $Ω$ , a boundary point $ζ$ , and local data $U$ and $q$ as in the Statement.

[L1]

A local strict peak function globalizes to a global barrier (A local strict subharmonic peak function globalizes).

[L2]

A boundary point is regular exactly when it admits a barrier (A boundary point is regular exactly when it admits a barrier).

Proof

technique · direct

1.1givenchoose

Choose a smaller neighbourhood $W ⋐ U$ of $ζ$ . The compact seam $(\overline{Ω \cap W}) \cap \partial W$ is a compact subset of $(\overline{Ω \cap U}) ∖ {ζ}$ , so hypothesis 3 gives [given, choose] $\sup_{η \in (\overline{Ω \cap W}) \cap \partial W} q^{\partial} (η) < 0.$ Thus $q$ is already a local strict peak function on $Ω \cap W$ .

2.1L1L2step 1.1∎

Applying [L1] to the restricted data on $W$ yields a global barrier at $ζ$ . Then [L2] shows that $ζ$ is regular.

Depends on

Used by

A boundary point whose complementary component contains another point is regular Lemma

Dependency tree · two levels

11 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

Harold P. Boas, Class Notes Math 618: Complex Variables II, Spring 2016 (standard reference, not scraped)