Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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 local strict subharmonic peak function globalizes

Statement

Let Ω⊆C be a bounded complex domain and let ζ∈∂Ω. Suppose there are a neighbourhood U of ζ and a subharmonic function q on Ω∩U such that:

  1. q(z)<0 for every z∈Ω∩U;
  2. q(z)→0 as z→ζ with z∈Ω;
  3. for some smaller neighbourhood W⋐U of ζ, one has sup⁡{q(z):z∈Ω∩∂W}<0.

Then Ω has a global barrier at ζ.

Facts & Assumptions

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

[L1]

Positive scalar multiples and finite maxima of subharmonic functions are subharmonic (Positive linear combinations and finite maxima preserve subharmonicity).

[L2]

Subharmonic pieces glue across a disc boundary under the limsup inequality (Subharmonic pieces glue across a boundary under the limsup inequality).

Proof

technique · direct
1.1L1givenchoose

Choose η>0 with q≤−η on Ω∩∂W, and then choose a constant c>0 so large that cq≤−1 on Ω∩∂W. The function cq is still subharmonic on Ω∩W by [L1], remains negative there, and still tends to 0 at ζ.

2.1L1L2step 1.1

Define [L1, L2, step 1.1] b(z)={max⁡{cq(z),−1},z∈Ω∩W,−1,z∈Ω∖W. Inside Ω∩W the function is subharmonic by [L1]. On the seam ∂W one has cq≤−1, so the inside limsup is at most the outside value −1; [L2] therefore glues the inside and outside pieces into a global subharmonic function on Ω.

3.1step 2.1∎

The function b is negative on Ω, tends to 0 at ζ because near ζ the maximum chooses the cq branch, and is identically −1 outside W, so it stays uniformly below a negative constant away from ζ. Thus b is a global barrier at ζ.

Depends on

Used by

Dependency tree · two levels

6 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