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.

The Poisson integral gives the unique continuous harmonic extension on the closed unit disc

Statement

Let $φ : \partial D \to R$ be continuous. Then its Poisson integral $P [φ]$ is harmonic on $D$ , extends continuously to $\overline{D}$ , agrees with $φ$ on $\partial D$ , and is the unique function with those properties.

Facts & Assumptions

Given: A continuous boundary datum $φ : \partial D \to R$ .

[L1]

The Poisson integral is harmonic on $D$ (Poisson integrals are harmonic on the unit disc).

[L2]

The Poisson integral converges to the boundary data uniformly as $r \to 1^{-}$ (The Poisson kernel is a boundary approximate identity).

[L3]

A bounded-domain continuous harmonic extension of fixed boundary data is unique (The bounded plane Dirichlet problem has at most one continuous harmonic solution).

Proof

technique · direct

1.1

By [L1], the function $P [φ]$ is harmonic on $D$ .

1.2

For $z = r e^{i α}$ with $0 \leq r < 1$ , [L2] gives $P [φ] (r e^{i α}) \to φ (e^{i α})$ uniformly in $α$ as $r \to 1^{-}$ . Therefore defining the boundary values of $P [φ]$ by $φ$ produces a continuous extension to $\overline{D}$ .

2.1

If $u$ is any other continuous harmonic function on $\overline{D}$ with $u = φ$ on $\partial D$ , then [L3] applied to $u$ and the extended Poisson integral forces $u = P [φ]$ on $\overline{D}$ .

step 1.1step 1.2L3∎

Depends on

Used by

Dependency tree · two levels

10 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

Sigurdur Helgason, MIT 18.112 Lecture 16: Harmonic Functions (standard reference, not scraped)