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.
Harmonic and holomorphic Schwarz reflection across the real axis
Statement
Write
- If is harmonic on , continuous on , and for every , then the odd reflection is harmonic on the full unit disc.
- If is holomorphic on , continuous on , and real-valued on , then the reflected function is holomorphic on the full unit disc.
Facts & Assumptions
Given: The upper half-disc .
The Poisson integral gives the unique continuous harmonic extension of continuous boundary data on a closed disc, and uniqueness holds on bounded domains with fixed boundary values (The Poisson integral gives the unique continuous harmonic extension on the closed unit disc, The bounded plane Dirichlet problem has at most one continuous harmonic solution).
On a star-shaped domain, every harmonic function has a harmonic conjugate, and a real-valued holomorphic function on a domain is constant (Star-shaped plane domains are homologically simply connected, Harmonic conjugates exist on homologically simply connected plane domains, A real-valued holomorphic function on a domain is constant).
Proof
For the harmonic statement, let satisfy the hypotheses, and define continuous boundary data on the unit circle by taking the upper semicircle values of and extending them oddly across the real axis. By [L1], has a harmonic Poisson extension to the full unit disc. On the upper half-disc, and are continuous harmonic functions with the same boundary values on the upper semicircle and on the diameter , so [L1] makes them equal there. By the odd construction of , the same harmonic function satisfies on the lower half-disc. Thus is exactly the reflected function , so is harmonic.
For the holomorphic statement, write on . Since is real-valued on , one has there; applying step 1.1 to gives a harmonic function on the full disc that equals above the axis and below it. Because the disc is star-shaped, [L2] gives a harmonic conjugate of , so is holomorphic. Multiplying by shows that is holomorphic and has imaginary part .
On , the holomorphic functions and have the same imaginary part , so their difference is real-valued and holomorphic; [L2] makes a real constant there. Subtracting that constant from , we may assume on .
For , the functions and have the same imaginary part . Their difference is therefore real-valued and holomorphic on the lower half-disc, hence constant by [L2]; continuity across the diameter, where both functions equal the same real boundary values, forces that constant to be . So below the axis, and the reflected function is holomorphic on the full disc.
Depends on
- The Poisson integral gives the unique continuous harmonic extension on the closed unit disc
- The bounded plane Dirichlet problem has at most one continuous harmonic solution
- Harmonic conjugates exist on homologically simply connected plane domains
- A real-valued holomorphic function on a domain is constant
- Star-shaped plane domains are homologically simply connected
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
32 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)
- Sigurdur Helgason, MIT 18.112 Lecture 16: Harmonic Functions (standard reference, not scraped)