TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-26

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.

An increasing harmonic sequence converges locally uniformly to a harmonic limit or diverges to +infinity

Statement

Let $(u_{n})$ be an increasing sequence of harmonic functions on a complex domain $Ω$ . Then exactly one of the following holds:

$u_{n} (z) \to + \infty$ for every $z \in Ω$ ;
there is a harmonic function $u$ on $Ω$ such that $u_{n} \to u$ locally uniformly on $Ω$ .

Facts & Assumptions

Given: An increasing sequence $(u_{n})$ of harmonic functions on a complex domain $Ω$ .

[L1]

Positive harmonic functions on a disc satisfy the Harnack inequality (Positive harmonic functions on a disc satisfy Harnack's inequality).

[L2]

Harmonic functions satisfy the mean-value property, and continuous functions with the local mean-value property are harmonic (Plane harmonic functions satisfy the mean-value property, A continuous plane function with the local mean-value property is harmonic).

[L3]

Open connected subsets of $R^{2}$ are polygonally connected (For an open subset of $R^{n}$ , connectedness, path-connectedness and polygonal connectedness are equivalent).

[L4]

Every increasing real sequence bounded above converges, and every real Cauchy sequence converges (A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum, The reals are complete).

Proof

technique · direct

1.1

If $u_{n} (z) \to + \infty$ for every $z \in Ω$ , then the first alternative holds and there is nothing to prove. Assume from now on that some $a \in Ω$ has $(u_{n} (a))$ bounded above; since the sequence is increasing, [L4] says that $u_{n} (a)$ converges to a finite real $L$ .

givenL4

2.1

Let $K \subseteq Ω$ be compact. By [L3], every point of $K$ can be joined to $a$ by a polygonal path in $Ω$ ; compactness yields finitely many discs with compact closure in $Ω$ whose overlaps form a chain from $a$ to a neighbourhood of each point of $K$ . Applying [L1] to the positive harmonic differences $u_{m} - u_{n}$ on each disc, one after another along the chain, bounds $\sup_{K} (u_{m} - u_{n})$ by a constant multiple of $(u_{m} (a) - u_{n} (a))$ . Since the latter tends to $0$ , the sequence is uniformly Cauchy on $K$ .

step 1.1L1L3

3.1

By step 2.1, $(u_{n} (z))$ is Cauchy for every $z$ , so [L4] defines $u (z) : = \lim_{n} u_{n} (z)$ . The same uniform-Cauchy estimate makes the convergence locally uniform, hence $u$ is continuous. Passing the circle mean-value identity of [L2] to the limit on every closed disc inside $Ω$ shows that $u$ still has the local mean-value property, and [L2] makes $u$ harmonic.

step 2.1L2L4

4.1

Thus, if the first alternative fails, the second holds. The two alternatives are exclusive because a locally uniform limit on any disc is finite there.

step 1.1step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

34 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

Encyclopedia of Mathematics, Harnack theorem (standard reference, not scraped)
Sigurdur Helgason, MIT 18.112 Lecture 16: Harmonic Functions (standard reference, not scraped)