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 logarithm of the modulus of a holomorphic function is subharmonic
Statement
Let be a complex domain and let be holomorphic on , not identically zero on any connected component. Define with the convention at the zeros of . Then is subharmonic on .
Facts & Assumptions
Given: A holomorphic function on a complex domain , not identically zero on any connected component.
A real function is subharmonic exactly when its Laplacian is nonnegative (A C^2 function is subharmonic exactly when its Laplacian is nonnegative).
Near a zero of order , the function factors as with holomorphic and (The order of a zero is the exponent in its local holomorphic factorization).
A holomorphic nonvanishing function on a disc has a holomorphic logarithm there (A nonvanishing holomorphic function on a disc has a holomorphic logarithm).
Holomorphic functions are smooth, so their real and imaginary parts admit the second derivatives used in [L1] (Holomorphic functions are real analytic and smooth in their two real coordinates).
Proof
Let be a disc on which has no zeros. By [L3], there is a holomorphic function on with . Writing , one has on . Since is holomorphic and smooth by [L4], the Cauchy-Riemann equations imply , so [L1] makes subharmonic on every zero-free disc.
Fix a zero of , and let . By [L2], on a small disc about one has with . Shrinking if necessary, has no zeros there, so step 1.1 makes harmonic and hence subharmonic on that disc.
On the punctured disc around , [step 2.1, algebra] The function is harmonic on the punctured disc, and at the center its value is while every circle average is finite; hence it is subharmonic there. Therefore the right-hand side is subharmonic on the whole disc, agreeing with away from and with at the center.
Every point of lies either on a zero-free disc covered by step 1.1 or on a zero-containing disc covered by step 3.1. So is subharmonic throughout .
Depends on
Used by
Dependency tree · two levels
29 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
- Harold P. Boas, Class Notes Math 618: Complex Variables II, Spring 2016 (standard reference, not scraped)