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.
Zero free entire function of exponential type is an exponential
Statement
Let be entire and zero-free, and suppose there are real constants and with
Then for all , where . In particular, if then .
The statement is deliberately formulated with the constant present: in applications the bound arises from a product in which the -dependent factor cannot be absorbed into the exponent without losing linearity in , and the constant factor is exactly what survives.
Facts & Assumptions
Given: The zero-free entire function and constants , of the statement.
On a convex complex domain every closed rectifiable contour integral of a holomorphic function vanishes; vanishing of these integrals for a continuous function is equivalent to existence of a primitive. (Cauchy's theorem on a convex complex domain, For a continuous function on a complex domain, endpoint independence, zero closed-contour integrals, and existence of a primitive are equivalent).
Holomorphic functions are exactly the locally analytic functions. Power-series sums are analytic and admit derivatives of every order by termwise differentiation; analytic functions are closed under algebraic operations, nonvanishing quotients and composition. (A complex function is holomorphic if and only if it is analytic, The sum of a complex power series is analytic throughout its open disc of convergence, A complex power-series sum has complex derivatives of every order, obtained by repeated termwise differentiation, Complex analytic functions are closed under finite linear combinations, products, quotients with nonzero denominator, and composition).
Complex derivatives satisfy the linear, product, quotient and chain rules; a holomorphic function with derivative zero on a domain is constant. (Linearity, product, reciprocal, and quotient rules for complex derivatives, The chain rule for complex derivatives, A holomorphic function with zero derivative on a domain is constant).
The complex exponential is entire with derivative itself, satisfies , agrees with the real exponential on the real axis and has modulus . The real exponential is a strictly increasing bijection onto the positive reals. (The complex exponential is entire and its complex derivative is itself, , and the complex exponential extends the real exponential, , , and , The exponential is a continuous bijection from onto , The exponential function is strictly increasing).
A function continuous on the closure of a bounded domain and holomorphic inside attains its maximum modulus on the boundary. Every bounded entire function is constant. (Boundary maximum modulus principle on a bounded domain, Liouville's theorem: every bounded entire function is constant).
Proof
A disk estimate including zero growth. Suppose is entire, , and with . Fix and , put and . For , the denominator has real part at least . Thus is holomorphic by [F2] and satisfies . For , , so . The local power series at zero shows that extends holomorphically through zero. For , [F5] applied on gives there; fixing and letting increase to one proves . Hence . At this becomes . Let decrease to zero to conclude ; at the same holds. In particular never produces division by zero, and forces .
Construct the entire logarithm. By the local power series and derivative statements of [F2], is holomorphic, and because is zero-free, is holomorphic. On the convex plane [F1] gives a primitive ; subtract its value at zero so and . A primitive is holomorphic by definition, so [F2] also supplies its local power series.
By [F3] and [F4], . Hence is constant with value , and the exponential addition formula gives . Here by zero-freeness.
The growth bound at zero gives . Let be the unique real number with , supplied by [F4]. Since the exponential is increasing and , . Taking moduli in step 2.1 and using [F4] gives , so . The disk estimate of step 1.1, applied directly to , yields for all .
Near zero write the convergent power series , with no constant term because . Then extends analytically through zero, with value ; the shifted series converges on the same disk by comparison on any smaller radius. Away from zero the quotient is holomorphic by [F2]. This defines an entire function , bounded by off zero by step 3.1 and at zero by continuity. By [F5], is constant and equals from step 1.2. Consequently with the stated , and step 2.1 gives .
If the bound in step 3.1 forces and hence and , including . If , step 4.1 gives the advertised normalized formula. The assumptions exclude and ; the removable value at zero and the open parameter limit have both been checked. All constructions use uniquely determined analytic operations or one primitive, not any simultaneous choice of arbitrary witnesses.
Depends on
- For a continuous function on a complex domain, endpoint independence, zero closed-contour integrals, and existence of a primitive are equivalent
- Cauchy's theorem on a convex complex domain
- Linearity, product, reciprocal, and quotient rules for complex derivatives
- The chain rule for complex derivatives
- A complex power-series sum has complex derivatives of every order, obtained by repeated termwise differentiation
- A holomorphic function with zero derivative on a domain is constant
- Liouville's theorem: every bounded entire function is constant
- Boundary maximum modulus principle on a bounded domain
- The sum of a complex power series is analytic throughout its open disc of convergence
- Complex analytic functions are closed under finite linear combinations, products, quotients with nonzero denominator, and composition
- A complex function is holomorphic if and only if it is analytic
- The complex exponential is entire and its complex derivative is itself
- $\exp(x+iy)=e^x(\cos y+i\sin y)$, $|\exp(x+iy)|=e^x$, and $e^{i\pi}+1=0$
- $\exp(z+w)=\exp z\,\exp w$, and the complex exponential extends the real exponential
- The exponential is a continuous bijection from $\mathbb{R}$ onto $(0,\infty)$
- The exponential function is strictly increasing
Used by
- Gleason Kahane Zelazko Theorem
Dependency tree · two levels
71 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
- Vahid Shirbisheh, Lectures on C-star Algebras, v2 — Lemma 3.1.10 (rescaled to a non-strict growth bound), printed pp. 58–59 (standard reference, not scraped)
- Theo Bühler and Dietmar A. Salamon, Functional Analysis — §5.5.1, printed pp. 258–267 (standard reference, not scraped)