LemmaStatement: 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.

Positive linear combinations and finite maxima preserve subharmonicity

Statement

Let $Ω \subseteq C$ be a complex domain.

If $u_{1}, \dots, u_{m}$ are subharmonic on $Ω$ and $α_{1}, \dots, α_{m} \geq 0$ , then $α_{1} u_{1} + \dots + α_{m} u_{m}$ is subharmonic on $Ω$ , where terms with $α_{j} = 0$ are omitted (so an all-zero combination is the zero function).
If $u_{1}, \dots, u_{m}$ are subharmonic on $Ω$ , then $u (z) = \max {u_{1} (z), \dots, u_{m} (z)}$ is subharmonic on $Ω$ .

Facts & Assumptions

Given: Subharmonic functions $u_{1}, \dots, u_{m}$ on a complex domain $Ω$ .

[L1]

Subharmonicity is equivalent to harmonic comparison on compactly contained discs (Subharmonicity is equivalent to harmonic comparison on compactly contained discs).

[L2]

The defining submean inequality for subharmonicity is linear in the function being averaged (Subharmonic functions on plane domains).

[L3]

A subharmonic function is finite almost everywhere (Plane subharmonic functions are locally integrable).

Proof

technique · direct

1.1

Let $I = {j : α_{j} > 0}$ . If $I$ is empty, the combination is the harmonic zero function. Otherwise it means the well-defined extended-real sum $\sum_{j \in I} α_{j} u_{j}$ ; no product $0 \cdot (- \infty)$ occurs. Finite sums with positive coefficients preserve upper semicontinuity, and [L3] shows that all summands are finite simultaneously almost everywhere, so their sum is not identically $- \infty$ . On any closed disc, multiply the submean inequality for $u_{j}$ by $α_{j} > 0$ and sum over $I$ to obtain the submean inequality for the combination.

givenL2L3algebra

1.2

For the finite maximum, upper semicontinuity is preserved by finite maxima. Let $\overline{D (a, r)} \subseteq Ω$ and let $h$ be continuous on the closure, harmonic on the disc, and satisfy $h \geq \max (u_{1}, \dots, u_{m})$ on the boundary. Then $h \geq u_{j}$ on the boundary for every $j$ , so [L1] gives $h \geq u_{j}$ throughout the disc for every $j$ . Therefore $h \geq \max (u_{1}, \dots, u_{m})$ on the disc. Another use of [L1] shows that the maximum is subharmonic.

L1given

2.1

Steps 1.1 and 1.2 prove the two closure properties.

step 1.1step 1.2∎

Depends on

Used by

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

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