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.
A nonvanishing holomorphic function on a disc has a holomorphic logarithm
Statement
If is nowhere zero and holomorphic on a disc, then there is a holomorphic on that disc with .
Precisely, if is an open disc with and is holomorphic and nowhere zero, then there is a holomorphic function satisfying for every .
Facts & Assumptions
Given: A disc with and a nowhere-zero holomorphic function on it. For and the triangle inequality gives , so every segment between two points of the disc stays in it; taking makes the disc star-shaped with respect to in the sense of Complex star-shaped and convex domains are the published Euclidean notions under the identification and Star-shaped open subsets of Euclidean space, and [L4] makes the disc a connected, hence a complex, domain. Also is itself holomorphic on the disc, because a holomorphic function has complex derivatives of all orders locally (All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle), so the quotient rule makes holomorphic there, being nowhere zero (Linearity, product, reciprocal, and quotient rules for complex derivatives); and the complex chain rule, the derivative of , and the exponential addition law are supplied by The chain rule for complex derivatives, The complex exponential is entire and its complex derivative is itself, and , and the complex exponential extends the real exponential.
Every holomorphic function on an open set star-shaped with respect to has a primitive there (Every holomorphic function on a star-shaped domain has a primitive).
A holomorphic function whose derivative vanishes everywhere on a complex domain is constant (A holomorphic function with zero derivative on a domain is constant).
For every nonzero complex number , the solutions of are exactly with (All logarithms of are , ).
A segment that lies in a subset is a continuous path in , and a path-connected subset of a topological space is a connected subset (A finite concatenation of straight segments in is a continuous path, Every path-connected space is connected, and every path component lies inside a component, claim 2).
Proof
By the star-shapedness in the Given and [L1], has a holomorphic primitive on the disc. Put ; then and .
The complex product and chain rules give , so, the disc being a complex domain by [L4], [L2] makes constant; its value at is .
Since , choose by [L3] a complex number with , and set .
The exponential addition law and step 2.1 give throughout the disc, so is the required holomorphic logarithm.
Depends on
- Every holomorphic function on a star-shaped domain has a primitive
- Star-shaped open subsets of Euclidean space
- All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle
- Linearity, product, reciprocal, and quotient rules for complex derivatives
- The chain rule for complex derivatives
- The complex exponential is entire and its complex derivative is itself
- $\exp(z+w)=\exp z\,\exp w$, and the complex exponential extends the real exponential
- A holomorphic function with zero derivative on a domain is constant
- All logarithms of $z\ne0$ are $\operatorname{Log}z+2\pi i k$, $k\in\mathbb Z$
- Complex star-shaped and convex domains are the published Euclidean notions under the identification $\mathbb C=\mathbb R^2$
- A finite concatenation of straight segments in $\mathbb{R}^n$ is a continuous path
- Every path-connected space is connected, and every path component lies inside a component
Used by
Dependency tree · two levels
55 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
- J. Lebl, Guide to Cultivating Complex Analysis, Corollary 4.3.4 (standard reference, not scraped)