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 be a bounded complex domain and let . Suppose there are a neighbourhood of and a subharmonic function on such that:
- for every ;
- as with ;
- for some smaller neighbourhood of , one has
Then has a global barrier at .
Facts & Assumptions
Given: A bounded complex domain , a boundary point , and local data , , and as in the Statement.
Positive scalar multiples and finite maxima of subharmonic functions are subharmonic (Positive linear combinations and finite maxima preserve subharmonicity).
Subharmonic pieces glue across a disc boundary under the limsup inequality (Subharmonic pieces glue across a boundary under the limsup inequality).
Proof
Choose with on , and then choose a constant so large that on . The function is still subharmonic on by [L1], remains negative there, and still tends to at .
Define [L1, L2, step 1.1] Inside the function is subharmonic by [L1]. On the seam one has , so the inside limsup is at most the outside value ; [L2] therefore glues the inside and outside pieces into a global subharmonic function on .
The function is negative on , tends to at because near the maximum chooses the branch, and is identically outside , so it stays uniformly below a negative constant away from . Thus 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
- Harold P. Boas, Class Notes Math 618: Complex Variables II, Spring 2016 (standard reference, not scraped)