TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)audited 2026-10-02

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.

Locally uniform limits of harmonic functions are smooth, with all derivatives converging

Statement

Assume Countable Choice and $n \geq 2$ . Let $Ω \subseteq R^{n}$ be open and let $u_{j} : Ω \to R$ or $C$ be harmonic with $u_{j} \to u$ locally uniformly on $Ω$ . Then $u$ is smooth and harmonic, and for every compact $K \subset Ω$ and every multi-index $α$ , $\sup_{x \in K} ∣ D^{α} u_{j} (x) - D^{α} u (x) ∣ ⟶ 0.$

Facts & Assumptions

Given: Countable Choice, an integer $n \geq 2$ , an open set $Ω \subseteq R^{n}$ , harmonic functions $u_{j}$ on $Ω$ converging locally uniformly to $u$ , a compact set $K \subset Ω$ and a multi-index $α$ .

[F1]

A locally uniform limit of harmonic functions is harmonic (Locally uniform limits of harmonic functions are harmonic).

[F2]

Every harmonic function is real analytic and hence $C^{\infty}$ , so all derivatives $D^{α} u$ exist (Harmonic functions are real analytic).

[F3]

Supremum Cauchy estimates: for harmonic $v$ on an open set containing $\overline{B_{ρ} (x)}$ , $∣ D^{α} v (x) ∣ \leq C_{n, α}^{'} ρ^{- ∣ α ∣} \sup_{B_{ρ} (x)} ∣ v ∣$ (Harmonic Cauchy estimates in supremum norm).

[F4]

A compact set and a disjoint closed set in a normed space keep a positive distance (A compact set and a disjoint closed set have a positive norm-distance gap), and a closed bounded subset of $R^{n}$ is compact (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[F5]

Countable Choice ${A C}_{ω}$ is the standing hypothesis (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct

1.1givenF1F2F5

Work under [F5]. By [F1] the limit $u$ is harmonic, and hence $C^{\infty}$ with all derivatives existing, by [F2].

2.1step 1.1F4cases

If $K = \emptyset$ , the uniform-convergence assertion on $K$ is vacuous, so assume $K \neq \emptyset$ . If $Ω \neq R^{n}$ , its complement is nonempty, closed and disjoint from $K$ , so [F4] gives $δ : = dist (K, R^{n} ∖ Ω) > 0$ ; put $ρ : = δ / 2$ . If $Ω = R^{n}$ , put $ρ : = 1$ . In either case let $K_{ρ} : = {x \in R^{n} : dist (x, K) \leq ρ}$ . Since $K$ is compact, it is bounded; the distance function is continuous, so $K_{ρ}$ is closed and bounded and hence compact by [F4]. In the first case $K_{ρ} \subseteq Ω$ , since every point of the complement has distance at least $δ$ from $K$ ; in the second case this inclusion is automatic. By local uniform convergence, $ε_{j} : = \sup_{K_{ρ}} ∣ u_{j} - u ∣ \to 0$ .

3.1step 1.1step 2.1F2F3

The difference $u_{j} - u$ is harmonic on $Ω \supseteq \overline{B_{ρ} (x)}$ for every $x \in K$ , so [F2] and [F3] give $∣ D^{α} u_{j} (x) - D^{α} u (x) ∣ \leq C_{n, α}^{'} ρ^{- ∣ α ∣} \sup_{B_{ρ} (x)} ∣ u_{j} - u ∣ \leq C_{n, α}^{'} ρ^{- ∣ α ∣} ε_{j}$ , a bound independent of $x \in K$ .

4.1step 3.1algebra

Taking the supremum over $x \in K$ in step 3.1 gives $\sup_{K} ∣ D^{α} u_{j} - D^{α} u ∣ \leq C_{n, α}^{'} ρ^{- ∣ α ∣} ε_{j} \to 0$ as $j \to \infty$ , for the arbitrary compact $K$ and multi-index $α$ ; this proves the derivative convergence.

5.1step 1.1step 4.1cases∎

Complex-valued $u_{j}$ are handled by applying the argument to real and imaginary parts, whose differences are harmonic and whose absolute values control $∣ D^{α} u_{j} - D^{α} u ∣ \leq ∣ D^{α} R e (u_{j} - u) ∣ + ∣ D^{α} I m (u_{j} - u) ∣$ ; the constant is doubled. Together with step 1.1 this proves that $u$ is smooth harmonic and that every derivative converges uniformly on compacta.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

67 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

John K. Hunter, Notes on Partial Differential Equations (2014) (standard reference, not scraped)
Sung-Jin Oh, Lecture Notes for Math 222A: Partial Differential Equations (2023) (standard reference, not scraped)