TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

Plane harmonicity is preserved by holomorphic and antiholomorphic changes of coordinate

Statement

Let $u$ be harmonic on an open set $V \subseteq C$ .

If $ϕ : U \to V$ is holomorphic on an open set $U$ , then $u \circ ϕ$ is harmonic on $U$ .
If $ψ : U \to V$ is antiholomorphic on an open set $U$ , then $u \circ ψ$ is harmonic on $U$ .

Facts & Assumptions

Given: A harmonic function $u$ on an open set $V$ .

[L1]

Near every point of $V$ , the function $u$ is the real part of a holomorphic function (Every plane harmonic function is locally the real part of a holomorphic function).

[L2]

Compositions of holomorphic functions are holomorphic (The chain rule for complex derivatives).

[L3]

A map is antiholomorphic exactly when its conjugate is holomorphic, and the same criterion shows that $w \mapsto \overline{F (\overline{w})}$ is holomorphic whenever $F$ is holomorphic (A conjugate difference quotient characterizes antiholomorphic maps).

Proof

technique · direct

1.1

For the holomorphic case, fix $a \in U$ . By [L1], choose a neighbourhood $W$ of $ϕ (a)$ and a holomorphic function $F$ on $W$ with $Re F = u$ there. Shrinking around $a$ if necessary, $ϕ$ maps that neighbourhood into $W$ , so [L2] makes $F \circ ϕ$ holomorphic and $Re (F \circ ϕ) = u \circ ϕ$ there. Thus $u \circ ϕ$ is harmonic near $a$ , and since $a$ was arbitrary it is harmonic on $U$ .

L1L2choose

2.1

For the antiholomorphic case, fix $a \in U$ and choose $W$ and $F$ as in step 1.1 around $ψ (a)$ . By [L3], the map $\tilde{ψ} (z) : = \overline{ψ (z)}$ is holomorphic on $U$ , and the map $\tilde{F} (w) : = \overline{F (\overline{w})}$ is holomorphic on $\overline{W} : = {\overline{ζ} : ζ \in W}$ . Therefore [L2] makes $\tilde{F} \circ \tilde{ψ}$ holomorphic on a neighbourhood of $a$ , and its real part is $Re \tilde{F} (\tilde{ψ} (z)) = Re \overline{F (ψ (z))} = Re F (ψ (z)) = u (ψ (z)) .$ Hence $u \circ ψ$ is harmonic near $a$ , and therefore on $U$ .

step 1.1L2L3

3.1

Steps 1.1 and 2.1 prove the two invariance statements.

step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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

Jeremy Orloff, MIT 18.04 Topic 5: Introduction to Harmonic Functions (standard reference, not scraped)