TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Maximum principle with limsup control at infinity

Statement

Let $n \geq 2$ , let $Ω \subseteq R^{n}$ be unbounded and open, and let $u \in C^{2} (Ω) \cap C (\overline{Ω})$ be subharmonic. Suppose $M \in R$ , $u \leq M$ on $\partial Ω$ , and ${lim sup}_{\begin{array}{c} x \in Ω \\ ∣ x ∣ \to \infty \end{array}} u (x) \leq M .$ Here the last condition means that for every $ε > 0$ there is $R_{0}$ with $u (x) \leq M + ε$ whenever $x \in Ω$ and $∣ x ∣ > R_{0}$ . Then $u \leq M$ on $\overline{Ω}$ , even if $\partial Ω$ is empty.

Facts & Assumptions

Given: The objects and hypotheses in the statement.

[F1]

A subharmonic $C^{2}$ function continuous on the closure of a bounded nonempty open set is bounded above by its boundary maximum. (Weak maximum principle for the laplacian).

Proof

technique · direct

1.1

Fix $x \in Ω$ and $ε > 0$ , choose $R_{0}$ from the infinity hypothesis, and choose $R > \max (R_{0}, ∣ x ∣)$ . The set $D = Ω \cap B_{R}$ is bounded nonempty open; its boundary lies in $(\partial Ω \cap {\overline{B}}_{R}) \cup (\overline{Ω} \cap \partial B_{R})$ .

given

2.1

On the first part $u \leq M$ . On the second part the infinity bound, extended from $Ω$ by continuity when necessary, gives $u \leq M + ε$ . The weak maximum principle on $D$ yields $u (x) \leq M + ε$ . Let $ε ↓ 0$ ; the original boundary inequality then also includes all closure points.

F1step 1.1algebra∎

Depends on

Weak maximum principle for the laplacian

Used by

Maximum principles need domain and boundary hypotheses Remark

Dependency tree · two levels

4 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

Thomas Schmidt, Lectures Notes, PDE (standard reference, not scraped)