TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 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.

Conformal transport of continuous Dirichlet solutions

Statement

Let $Ω, Ω^{'} \subseteq C$ be bounded regular complex domains, let $F : Ω \to Ω^{'}$ be a conformal bijection that extends to a homeomorphism $\overline{Ω} \to \overline{Ω^{'}}$ , and let $φ : \partial Ω^{'} \to R$ be continuous. If $u$ is the unique continuous harmonic function on $\overline{Ω}$ with boundary data $φ \circ F ∣_{\partial Ω}$ , then $v : = u \circ F^{- 1}$ is the unique continuous harmonic function on $\overline{Ω^{'}}$ with boundary data $φ$ .

Facts & Assumptions

Given: Bounded regular complex domains $Ω, Ω^{'}$ , a closure-homeomorphic conformal bijection $F : Ω \to Ω^{'}$ , and a continuous boundary datum $φ : \partial Ω^{'} \to R$ .

[L1]

On a regular bounded plane domain, Perron's method gives the unique continuous harmonic solution of the Dirichlet problem (On a regular bounded plane domain, Perron's method solves the Dirichlet problem).

[L2]

Harmonicity is preserved under holomorphic changes of coordinate (Plane harmonicity is preserved by holomorphic and antiholomorphic changes of coordinate).

[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 source datum $φ \circ F ∣_{\partial Ω}$ has a unique continuous harmonic solution $u$ on $\overline{Ω}$ . Define $v = u \circ F^{- 1}$ on $Ω^{'}$ . Since $F^{- 1}$ is holomorphic on $Ω^{'}$ , [L2] makes $v$ harmonic on $Ω^{'}$ .

L1L2given

2.1

The homeomorphic extension of $F$ to the closures shows that $F^{- 1}$ extends continuously from $\overline{Ω^{'}}$ to $\overline{Ω}$ . Therefore $v$ extends continuously to $\overline{Ω^{'}}$ , and for $ξ \in \partial Ω^{'}$ one has [step 1.1, given] $v (ξ) = u (F^{- 1} (ξ)) = (φ \circ F) (F^{- 1} (ξ)) = φ (ξ) .$ This identifies the transported boundary values.

step 1.1given

3.1

Let $w$ be any other continuous harmonic function on $\overline{Ω^{'}}$ with boundary data $φ$ . Then $w \circ F$ is continuous on $\overline{Ω}$ , harmonic on $Ω$ by [L2], and has boundary values $φ \circ F$ on $\partial Ω$ . By [L3], one has $w \circ F = u$ on $\overline{Ω}$ , hence $w = v$ on $\overline{Ω^{'}}$ .

L2L3step 2.1

4.1

Thus $v = u \circ F^{- 1}$ is exactly the unique Dirichlet solution on $Ω^{'}$ with boundary data $φ$ .

step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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

Boris Khoruzhenko, Potential Theory lecture notes (standard reference, not scraped)