TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

The upper-semicontinuous regularization of a locally bounded-above subharmonic supremum is subharmonic

Statement

Let $F$ be a nonempty family of subharmonic functions on a complex domain $Ω$ , and suppose that for every compact set $K \subseteq Ω$ there is a real number $M_{K}$ with $v \leq M_{K}$ on $K$ for every $v \in F$ . Define $u (z) = \sup_{v \in F} v (z), U = u^{*} .$ Then $U$ is subharmonic on $Ω$ .

Facts & Assumptions

Given: A locally bounded-above family $F$ of subharmonic functions on a complex domain $Ω$ .

[L1]

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

[L2]

A function is subharmonic exactly when every harmonic boundary majorant on a compactly contained disc majorizes it throughout that disc (Subharmonicity is equivalent to harmonic comparison on compactly contained discs).

[L3]

Upper-semicontinuous regularization is the least upper-semicontinuous majorant (Upper-semicontinuous regularization).

Proof

technique · direct

1.1

For every compact set $K \subseteq Ω$ , the hypothesis gives a real number $M_{K}$ with $u \leq M_{K}$ on $K$ , so both $u$ and $U = u^{*}$ are locally bounded above and never take the value $+ \infty$ . Because $F$ is nonempty and every $v \in F$ satisfies $v \leq u \leq U$ , the function $U$ is not identically $- \infty$ on any connected component. By [L3], $U$ is upper semicontinuous and satisfies $u \leq U$ .

givenL3

2.1

Let $\overline{D (a, r)} \subseteq Ω$ and let $h$ be continuous on the closure, harmonic on the disc, and satisfy $h \geq U$ on $\partial D (a, r)$ . Because $u \leq U$ , one also has $h \geq u$ on the boundary.

step 1.1given

3.1

Fix any $v \in F$ . Since $h \geq v$ on $\partial D (a, r)$ , [L2] gives $h \geq v$ on $D (a, r)$ . The same is therefore true for every finite maximum of members of $F$ , and [L1] keeps those maxima subharmonic. Taking the supremum over all $v \in F$ yields $h \geq u$ on $D (a, r)$ .

L1L2step 2.1

4.1

Since $h$ is continuous and dominates $u$ , it also dominates the least upper-semicontinuous majorant $U$ by [L3]. Thus $h \geq U$ on $D (a, r)$ . Another use of [L2] shows that $U$ is subharmonic on $Ω$ .

L2L3step 3.1∎

Depends on

Used by

FALSE: an arbitrary pointwise supremum of subharmonic functions is subharmonic False statement
The regularized Perron envelope is harmonic Theorem

Dependency tree · two levels

12 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

Sheldon Axler, Paul Bourdon, and Wade Ramey, Harmonic Function Theory, 2nd ed. (standard reference, not scraped)