Alphabeta Math
Pipeline-generated
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.

14 results · all verified · 3 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 11 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Infinite Products and the Weierstrass Factorisation Theorem

1 · Prerequisites

2 · Summary

This page reuses the published tail-based infinite-product convention and then adapts it to holomorphic function theory. After the absolute-convergence and normal-convergence criteria, the core estimate for Weierstrass elementary factors drives the canonical-product construction, the plane zero-divisor theorem, and the factorization of every entire function into its zeros and a zero-free exponential factor.

The second half measures how zero distributions constrain growth. Jensen's formula turns boundary size into zero counts, the order of an entire function captures the asymptotic growth class, and Hadamard's theorem upgrades the Weierstrass factorization to a finite-order factorization with polynomial exponential term. The sine product sits in the middle as the worked canonical example that links the abstract machinery back to a classical function.

3 · Logical flowchart

4 · Definitions, theorems and proofs

RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Complex infinite-product convention extending the published real definition

Remark

The published definition Infinite products: partial products, and convergence to a nonzero limit after finitely many vanishing factors is stated for real factors. This page extends its tail convention explicitly to complex factors: for a complex sequence (bn), the product n0bn converges when there is an index N such that bn0 for every nN and the complex partial products n=Nmbn converge as m to a nonzero complex limit.

For a complex sequence (an), the phrase

n0(1+an) converges absolutely

means exactly that the real product

n0(1+an)

converges in the sense of Infinite products: partial products, and convergence to a nonzero limit after finitely many vanishing factors. By For pk0 the product (1+pk) converges iff pk converges, with 1+k<npkk<n(1+pk)1/(1k<npk) when k<npk<1; for 0pk<1 the product (1pk) converges iff pk converges and its partial products tend to 0 otherwise; and pk convergent implies (1+pk) convergent, this is equivalent to the numerical series n0an converging.

The zero-factor convention is also unchanged. A finite number of zero factors is harmless because convergence is tail-based, but infinitely many zero factors prevent any admissible nonzero tail limit. Later theorems will therefore isolate finite zero sets first and then work on zero-free tails.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

Absolute convergence criterion for complex infinite products

Statement

Let (an)n0 be a sequence of complex numbers. The following are equivalent:

  1. the product n0(1+an) is absolutely convergent, meaning that n0(1+an) converges;
  2. the series n0an converges.

When these conditions hold, the complex product n0(1+an) itself converges and has nonzero value.

Facts & Assumptions

Given: A complex sequence (an).

[F1]

Absolute convergence of (1+an) means convergence of the real product (1+an) (Complex infinite-product convention extending the published real definition).

[F3]

An infinite product converges when some tail has nonzero factors and a nonzero tail-product limit (Infinite products: partial products, and convergence to a nonzero limit after finitely many vanishing factors).

Proof

technique · direct
1.1

By [F1], absolute convergence of (1+an) is exactly convergence of the real product (1+an), and [F2] makes that equivalent to convergence of an. This proves the equivalence of claims 1 and 2.

F1F2given
1.2

Assume now that an converges. By [F2], choose N so that nNan<1/2; then an<1/2 for every nN, so 1+an0 on that tail.

F2choosealgebra
2.1

For m>nN one has k=nm(1+ak)1k=nm(1+ak)1, and the right-hand side tends to 0 as n,m because the real tail products converge by [F2]. Hence the complex tail partial products form a Cauchy sequence, so they converge to some limit C.

F2step 1.2algebra
3.1

For the same tail, 1+an1an>0, so k=Nm(1+ak)k=Nm(1ak) for every mN; by [F2], the real product kN(1ak) converges to a positive limit because kNak converges and each term is in [0,1/2). Therefore the complex tail partial products are bounded away from 0, so the limit of step 2.1 is nonzero. Now [F3] makes (1+an) convergent with nonzero value.

F2F3step 1.2step 2.1algebra
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Normal convergence of holomorphic products

Definition

Let ΩC be open, and let fn:ΩC be holomorphic functions for n0.

The product

n0fn(z)

is normally convergent on Ω if for every compact set KΩ there is an integer N such that fn has no zero on K for all nN and

nNsupzKfn(z)1<.

Equivalently, after discarding finitely many factors that may contribute zeros, the deviations from 1 are absolutely summable uniformly on each compact set. This is the product analogue of normal convergence for holomorphic series.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Normally convergent products define holomorphic functions with the expected zeros

Statement

Let ΩC be open, and let (fn)n0 be holomorphic functions on Ω whose product is normally convergent in the sense of Normal convergence of holomorphic products. Assume moreover that no factor fn is identically zero on Ω. Then the partial products

Pm(z):=n=0mfn(z)

converge locally uniformly on Ω to a holomorphic function F.

Moreover, on every compact set KΩ, all but finitely many factors fn are zero-free and the tail limit is zero-free; therefore the zeros of F on K, counted with multiplicity, are exactly those contributed by the finitely many exceptional factors.

Facts & Assumptions

Given: An open set Ω and a normally convergent holomorphic product fn on Ω, with no factor fn identically zero on Ω.

[F1]

Normal convergence means that on each compact KΩ there is an index N such that fn has no zero on K for nN and nNsupKfn1< (Normal convergence of holomorphic products).

[F2]

If an converges, then (1+an) converges and has nonzero value (Absolute convergence criterion for complex infinite products).

[F4]

Multiplication by a holomorphic factor that is nonzero at a point does not change the order of a zero there (The order of a zero is the exponent in its local holomorphic factorization).

Proof

technique · direct
1.1

Fix a compact set KΩ. By [F1], choose N so that fn has no zero on K for nN and Mn:=supKfn1 satisfies nNMn<; enlarging N if needed, assume also Mn<1/2 for nN.

F1givenchoose
2.1

For mN and zK, one has n=mfn(z)1n=m(1+Mn)1, while fn(z)1Mn for nN. By [F2], the real products nN(1+Mn) and nN(1Mn) converge, so the tail partial products of fn are uniformly bounded above and uniformly bounded away from 0 on K.

F2step 1.1algebra
3.1

The estimate of step 2.1 implies that the tail partial products are uniformly Cauchy on K, hence converge uniformly there to a continuous zero-free limit QK; multiplying by the finite holomorphic prefix n<Nfn gives uniform convergence of the full partial products on K. Because K was arbitrary, the convergence is locally uniform on Ω, and [F3] makes the limit function F holomorphic.

F2F3step 2.1algebra
4.1

On the fixed compact set K, write F=(n<Nfn)QK with QK holomorphic and zero-free by step 3.1. Because no factor fn is identically zero on Ω, the finitely many prefix factors have only isolated zeros, and [F4] shows that every zero of F on K, with its multiplicity, comes from that finite prefix and no tail factor contributes a new zero.

F4step 1.1step 3.1givenalgebra
CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

The logarithmic derivative of a normally convergent product

Statement

Let n0fn be a normally convergent holomorphic product on an open set Ω, and let F be its holomorphic limit. On every compact set KΩ disjoint from the zero set of F, the series

n0fn(z)fn(z)

converges uniformly on K and

F(z)F(z)=n0fn(z)fn(z)(zK).

Facts & Assumptions

Given: A normally convergent product fn on Ω with limit F.

[F1]

A normally convergent product has a holomorphic limit, and on each compact set only finitely many factors contribute zeros (Normally convergent products define holomorphic functions with the expected zeros).

[F2]

Locally uniform convergence of holomorphic functions carries locally uniform derivative convergence (Locally uniform limits of holomorphic functions are holomorphic and their derivatives converge locally uniformly).

Proof

technique · direct
1.1

Fix a compact set KΩ disjoint from the zero set of F. By [F1], choose N so that fn has no zero on K for nN, and write Pm=n=0mfn. Then PmF uniformly on K, and for mN the functions Pm are zero-free on K.

F1givenchoose
2.1

By [F2], the derivatives Pm converge uniformly on K to F. Since F has no zero on the compact set K, the uniform convergence of Pm to F makes Pm uniformly bounded away from 0 on K for all large m, so Pm/PmF/F uniformly on K.

F2step 1.1algebra
3.1

For each finite product, ordinary differentiation gives Pm/Pm=n=0mfn/fn on K. Passing to the uniform limit from step 2.1 yields the stated series identity and uniform convergence.

step 2.1algebra
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Weierstrass elementary factors

Definition

For an integer p0, the pth Weierstrass elementary factor is

Ep(w):=(1w)exp ⁣(w+w22++wpp).

For p=0 the empty sum in the exponential is interpreted as 0, so E0(w)=1w.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

The unit-disc estimate for Weierstrass elementary factors

Statement

For every integer p0 and every complex number w with w1,

1Ep(w)wp+1.

In particular, there is a universal constant C=1 such that

1Ep(w)Cwp+1(w1).

Facts & Assumptions

Given: An integer p0.

[F1]

The elementary factor is Ep(w)=(1w)exp ⁣(w+w22++wpp) (Weierstrass elementary factors).

[F3]

Complex derivatives satisfy the linearity and product rules (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[F4]

Complex derivatives satisfy the chain rule (The chain rule for complex derivatives).

Proof

technique · direct
1.1

Write Sp(u)=u+u2/2++up/p, with the empty sum 0 when p=0. Using [F1], [F2], [F3], and [F4], differentiate Ep(u)=(1u)eSp(u) to obtain Ep(u)=eSp(u)+(1u)eSp(u)(1+u++up1)=upeSp(u).

F1F2F3F4givenalgebra
2.1

Fix w with w1. By step 1.1, ddtEp(tw)=wEp(tw)=wp+1tpeSp(tw)(0t1). Integrating from 0 to 1 and using Ep(0)=1 gives 1Ep(w)=wp+101tpeSp(tw)dt.

F1step 1.1algebra
3.1

For 0t1 and 1kp, one has Re ⁣((tw)kk)twkktkk, so eSp(tw)=eReSp(tw)eSp(t). Taking absolute values in step 2.1 therefore yields 1Ep(w)wp+101tpeSp(t)dt.

step 2.1algebra
4.1

For real t[0,1], step 1.1 gives ddtEp(t)=tpeSp(t). Hence 01tpeSp(t)dt=Ep(0)Ep(1)=1, because Ep(0)=1 and Ep(1)=0 by [F1]. Substituting this into step 3.1 proves 1Ep(w)wp+1, and the displayed bound with C=1 follows.

F1step 1.1step 3.1algebra
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Weierstrass products, canonical products, and genus

Definition

Let (an)n1 be a sequence of nonzero complex numbers with no finite accumulation point, and let (pn)n1 be integers with pn0.

Finite zero multisets are allowed as a separate degenerate case: the associated products have only finitely many factors, the empty product is 1, and their canonical genus is defined to be 0.

The product

n1Epn(z/an)

is a Weierstrass product for the zero sequence (an).

If one integer p0 is used for every factor, so the product is

n1Ep(z/an),

it is the canonical product of genus p associated to (an). If there is at least one integer p0 for which that canonical product converges, the least such p is the canonical genus of the sequence. If no such integer exists, its canonical genus is +.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

The exponent of convergence of a zero sequence

Definition

Let (an)n1 be a sequence of nonzero complex numbers with no finite accumulation point. The exponent of convergence of (an) is

λ:=inf{s>0:n1ans<}[0,].

Equivalently, λ is the threshold between convergence and divergence of the reciprocal power sums.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

A canonical product converges when the (p+1)-power reciprocal sum converges

Statement

Let (an)n1 be a sequence of nonzero complex numbers with no finite accumulation point, and fix an integer p0. If

n1an(p+1)<,

then the canonical product

n1Ep(z/an)

converges normally on C and therefore defines an entire function whose zeros are exactly the points an, counted with multiplicity.

Facts & Assumptions

Given: The sequence (an) and the integer p0.

[F1]

The factor estimate gives 1Ep(w)ewp+1 for w1 (The unit-disc estimate for Weierstrass elementary factors).

[F2]

Canonical products are the fixed-genus Weierstrass products (Weierstrass products, canonical products, and genus).

[F3]

A normally convergent holomorphic product defines a holomorphic function with exactly the zeros contributed by the finitely many nonzero exceptional factors on each compact set (Normally convergent products define holomorphic functions with the expected zeros).

Proof

technique · direct
1.1

Fix a compact disc KR={z:zR}. Since (an) has no finite accumulation point, an, so there is N with an>R for nN; then z/an1 on KR for every nN.

givenchoose
2.1

For zKR and nN, [F1] gives 1Ep(z/an)z/anp+1Rp+1an(p+1). Because the reciprocal power series converges, the Weierstrass M-test makes nNsupzKR1Ep(z/an) convergent.

F1step 1.1algebra
3.1

By [F2], the product n1Ep(z/an) is a canonical product, and step 2.1 is exactly the normal-convergence condition on the arbitrary compact disc KR. Hence [F3] makes the product entire, with zeros exactly at the points an and with their multiplicities.

F2F3step 2.1algebra
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

Weierstrass product theorem on the complex plane

Statement

Let m0 be an integer, and let (an)n1 be a sequence of nonzero complex numbers with no finite accumulation point, where each value may repeat according to its intended multiplicity. Then there are integers pn0 such that

P(z):=zmn1Epn(z/an)

converges normally on C and is entire, with zero set exactly {0} of order m together with the nonzero zeros an counted with multiplicity.

Facts & Assumptions

Given: The integer m0 and the sequence (an).

[F1]

A Weierstrass product is a product of elementary factors with varying orders (Weierstrass products, canonical products, and genus).

[F2]

For every integer p0 and w1, the elementary factor satisfies 1Ep(w)wp+1 (The unit-disc estimate for Weierstrass elementary factors).

[F3]

A normally convergent holomorphic product defines an entire function whose zeros on each compact set are exactly those contributed by the finitely many exceptional factors (Normally convergent products define holomorphic functions with the expected zeros).

Proof

technique · direct
1.1

Set pn:=n for every n1. Fix R>0. Because (an) has no finite accumulation point, only finitely many terms satisfy an2R; choose N so that an>2R for all nN.

givenchooseconstruct
2.1

For zR and nN, one has z/anR/an<1/21, and En(z/an)0 because its unique zero occurs at z=an, outside the closed disc zR. Using [F2] with p=n gives 1En(z/an)z/ann+1(R/an)n+12n1. Therefore nNsupzR1En(z/an) converges.

F2step 1.1algebra
3.1

Step 2.1 is exactly the normal-convergence condition on the closed disc zR, and R was arbitrary. Hence [F3] makes n1En(z/an) an entire function whose zeros are exactly the points an, counted with multiplicity. Multiplying by zm contributes precisely the order-m zero at 0 and no other zeros, so P(z)=zmn1En(z/an) has exactly the stated zero divisor. Since pn=n0, this is a Weierstrass product in the sense of [F1].

F1F3step 2.1algebra
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

Weierstrass factorization for entire functions

Statement

Let f be an entire function, not identically zero, and let m be the order of its zero at 0. If f has infinitely many nonzero zeros, let (an)n1 list them with multiplicity and without finite accumulation point. Then there is an entire function g such that

f(z)=zmeg(z)n1Epn(z/an)

for suitable integers pn0.

If f has finitely many nonzero zeros a1,,aN, the corresponding conclusion is

f(z)=zmeg(z)j=1NE0(z/aj),

where the product is 1 when N=0.

Facts & Assumptions

Given: A nonzero entire function f.

[F1]

The zero at 0 has finite order m, and locally one can factor off (za)m from a holomorphic function according to its zero multiplicity (The order of a zero is the exponent in its local holomorphic factorization).

[F2]

The Weierstrass product theorem constructs an entire product with any prescribed discrete zero divisor on C (Weierstrass product theorem on the complex plane).

[F3]

The plane C is star-shaped and therefore homologically simply connected (Star-shaped plane domains are homologically simply connected).

[F4]

A nowhere-zero holomorphic function on a homologically simply connected domain has a holomorphic logarithm (A nonvanishing holomorphic function on a homologically simply connected domain has a holomorphic logarithm).

[F5]

The elementary factor E0(w)=1w has its unique zero at w=1. (Weierstrass elementary factors)

Proof

technique · direct
1.1

Let m be the order of the zero of f at 0, with m=0 if f(0)0. If the nonzero zero multiset is infinite, [F2] gives an entire function P(z)=zmn1Epn(z/an) with exactly the same zeros as f, counted with multiplicity. If it is finite, list it as a1,,aN and put P(z)=zmj=1NE0(z/aj), with the empty product equal to 1; [F5] gives the same zero-divisor conclusion.

F1F2F5givenconstructcases
2.1

The quotient h=f/P is holomorphic on C: away from the common zeros this is immediate, and at each zero the matching multiplicities from step 1.1 and [F1] remove the singularity. Moreover h has no zero anywhere, because every zero of f was already cancelled by P.

F1F2step 1.1algebra
3.1

By [F3], the whole plane is homologically simply connected, so [F4] gives an entire function g with eg=h. Substituting the definition of h from step 2.1 yields the required infinite or finite factorization of f.

F3F4step 2.1algebra
CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

Every meromorphic function on C is a quotient of entire functions

Statement

Every meromorphic function on C is a quotient of entire functions.

Facts & Assumptions

Given: A meromorphic function f on C.

[F1]

A meromorphic function on a plane domain is holomorphic off a discrete pole set, and each pole is an isolated pole in the usual sense (Meromorphic functions on a plane domain).

[F2]

The Weierstrass product theorem constructs an entire function with any prescribed discrete zero divisor on C (Weierstrass product theorem on the complex plane).

[F3]

A bounded punctured-neighbourhood singularity is removable (Characterizations of removable singularities).

Proof

technique · direct
1.1

Let (pn) be the poles of f, listed with multiplicity equal to the order of the pole. By [F2], there is an entire function q whose zeros are exactly the points pn with those multiplicities and with no other zeros.

F1F2givenconstruct
2.1

On C{pn} define g=fq. Near a pole pn of order m, the zero of q has the same order m, so the product g is locally bounded on the punctured neighbourhood of pn. By [F3], each such singularity is removable, hence g extends to an entire function on C.

F1F3step 1.1algebra
3.1

Away from the poles, f=g/q by construction, and both sides are meromorphic with the same removed singularities at the poles. Therefore f is the quotient of the two entire functions g and q.

step 1.1step 2.1algebra
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

The Weierstrass product for sine

Statement

For every complex number z,

sin(πz)=πzn1(1z2n2),

with locally uniform convergence on C.

Facts & Assumptions

Given: The entire function f(z)=sin(πz).

[F1]

The zeros of complex sine are exactly the integer multiples of π, so the zeros of f(z)=sin(πz) are exactly the integers, with 0 simple and the nonzero zeros occurring in the pairs ±n (The zeros of complex sine are the integer multiples of pi, and the zeros of complex cosine are the odd half-integer multiples of pi).

[F2]

Hadamard factorization applies to finite-order entire functions (Hadamard factorization for finite-order entire functions).

[F3]

The order of an entire function is computed from the growth of its maximum modulus (The order of an entire function).

[F4]

Complex sine is defined from the exponential, and its entire power series is sinz=k0(1)kz2k+1(2k+1)! (Complex sine, cosine, hyperbolic sine, and hyperbolic cosine from the complex exponential, The exponential definitions of complex sine, cosine, hyperbolic sine, and hyperbolic cosine equal their entire power series).

Proof

technique · direct
1.1

For z=x+iy, [F4] gives sin(πz)=(eiπzeiπz)/(2i), so sin(πz)12(eπy+eπy)eπz. Along the imaginary axis one has sin(πir)=(eπreπr)/2 for r>0. Therefore [F3] makes f(z)=sin(πz) an entire function of order 1.

F3F4givenalgebra
2.1

By [F1], the zero at 0 has order 1 and the nonzero zeros are exactly ±1,±2,. Applying [F2] with ρ=1 yields a polynomial Q of degree at most 1 such that sin(πz)=zeQ(z)n1E1(z/n)E1(z/n). Since E1(w)E1(w)=(1w)ew(1+w)ew=1w2, this becomes sin(πz)=zeQ(z)n1(1z2/n2).

F1F2step 1.1algebra
3.1

By [F4], the function sin(πz) is odd, while n1(1z2/n2) is even. Therefore the quotient eQ(z)=sin(πz)zn1(1z2/n2) is even. Writing Q(z)=az+b, this means eaz+b=eaz+b for every z, so e2az=1 on C. Therefore a=0, and Q is constant.

F4step 2.1algebra
4.1

Dividing the power series in [F4] by πz gives sin(πz)/(πz)=1π2z2/6+O(z4). Step 2.1 with step 3.1 gives sin(πz)/z=ebn1(1z2/n2), and substituting z=0 shows eb=π. Therefore sin(πz)=πzn1(1z2/n2). The convergence is locally uniform because step 2.1 is a normally convergent canonical-product factorization.

F4step 2.1step 3.1algebra
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Jensen's formula on a disc

Statement

Let f be holomorphic on a neighbourhood of the closed disc {zR}, assume f(0)0, and let a1,,aN be the zeros of f in z<R, counted with multiplicity. If f has no zero on z=R, then

logf(0)=12π02πlogf(Reit)dtk=1NlogRak.

For a radius meeting boundary zeros, the same identity is recovered by taking rR through radii that avoid zeros on z=r.

Facts & Assumptions

Given: A holomorphic function f on a neighbourhood of the closed disc {zR}, with f(0)0.

[F1]

Cauchy's integral formula on a circle recovers the value at the centre (Cauchy's integral formula on a circle compactly contained in a disc of holomorphy).

[F2]

A zero of multiplicity m can be factored as (za)m times a holomorphic nonvanishing factor (The order of a zero is the exponent in its local holomorphic factorization).

[F3]

A nowhere-zero holomorphic function on a disc has a holomorphic logarithm, because discs are star-shaped and homologically simply connected (Star-shaped plane domains are homologically simply connected, A nonvanishing holomorphic function on a homologically simply connected domain has a holomorphic logarithm).

Proof

technique · direct
1.1

Assume first that f has no zero on z=R. Because the closed disc is compact, f has only finitely many zeros in z<R; applying [F2] repeatedly gives f(z)=k=1N(zak)g(z) on a neighbourhood of the closed disc, where g is holomorphic and zero-free there.

F2givenalgebra
2.1

By [F3], choose a holomorphic logarithm L of g on z<R. Applying [F1] to L on the circle z=R and taking real parts yields logg(0)=12π02πlogg(Reit)dt.

F1F3step 1.1algebra
3.1

For each zero ak with ak<R, write Reitak=Reit(1akR1eit). The factor 1akR1z is zero-free on the closed unit disc, so the same argument as in step 2.1 shows 12π02πlog1akR1eitdt=0; hence 12π02πlogReitakdt=logR.

F1F3step 2.1algebra
4.1

Taking logarithms of the factorization in step 1.1 on the boundary circle and averaging, step 2.1 gives the mean for g and step 3.1 contributes one logR for each zero. Rearranging yields logf(0)=12π02πlogf(Reit)dtk=1Nlog(R/ak).

step 1.1step 2.1step 3.1algebra
5.1

If f has zeros on z=R, apply step 4.1 to radii r<R with no zero on z=r; as rR, the zero list inside z<r stabilizes except when r crosses one of finitely many zero moduli, and the boundary integral converges to the stated radial limit.

step 4.1algebra
CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

Jensen's formula bounds the number of zeros in a smaller disc

Statement

Let f be holomorphic on a neighbourhood of the closed disc {zR}, assume f(0)0, and let n(r) denote the number of zeros of f in zr, counted with multiplicity, for 0<r<R. Then

n(r)logRr12π02πlogf(Reit)dtlogf(0).

Facts & Assumptions

Given: A holomorphic function f on a neighbourhood of the closed disc {zR} with f(0)0, and a radius 0<r<R.

[F1]

Jensen's formula gives logf(0)=12π02πlogf(Reit)dtk=1NlogRak for the zeros ak of f in z<R (Jensen's formula on a disc).

Proof

technique · direct
1.1

If ak is a zero with akr, then log(R/ak)log(R/r). There are exactly n(r) such zeros, counted with multiplicity.

givenalgebra
2.1

Therefore the Jensen sum in [F1] satisfies k=1Nlog(R/ak)n(r)log(R/r). Substituting this lower bound into [F1] and rearranging gives the stated inequality.

F1step 1.1algebra
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

The order of an entire function

Definition

Let f be entire and put

Mf(r):=maxz=rf(z)(r>0).

The order of f is

ρ(f):=lim suprloglogMf(r)logr,

with the convention that a constant nonzero entire function has order 0 and the zero function is left outside this definition unless stated otherwise.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

The exponent of convergence of the zeros of an entire function does not exceed its order

Statement

Let f be a nonzero entire function of finite order ρ. For a finite multiset of nonzero zeros, use the convention that its exponent of convergence is 0. If the nonzero zero multiset is infinite, let (an)n1 list it with multiplicity and without finite accumulation point. In either case the exponent of convergence satisfies

λρ.

Equivalently, for every real s>ρ the reciprocal power sum over all nonzero zeros, counted with multiplicity, is finite; in the infinite case this is

n1ans<.

Facts & Assumptions

Given: A nonzero entire function f of order ρ< and its nonzero zero multiset, enumerated as (an) when it is infinite.

[F1]

The order is the limsup growth rate of loglogMf(r) (The order of an entire function).

[F2]

Jensen's counting corollary bounds the number n(r) of zeros in zr in terms of the boundary growth on a larger circle (Jensen's formula bounds the number of zeros in a smaller disc).

[F3]

The exponent of convergence is the infimum threshold for convergence of the reciprocal power sums (The exponent of convergence of a zero sequence).

[F4]

A zero of finite order can be factored off locally as a power of z times a holomorphic function nonvanishing at 0 (The order of a zero is the exponent in its local holomorphic factorization).

Proof

technique · direct
1.1

Let m be the order of the zero of f at 0, with m=0 if f(0)0. By [F4], there is an entire function g with g(0)0 and f(z)=zmg(z), so g has exactly the same nonzero zeros as f, with the same multiplicities.

F4givenconstruct
1.2

If that nonzero zero multiset is finite, every reciprocal power sum over it is finite and its exponent is 0ρ, so the conclusion holds. Hence assume from now on that it is infinite and enumerate it as (an)n1.

step 1.1givencases
2.1

For r1 and z=r, step 1.1 gives g(z)=f(z)/rmf(z), hence Mg(r)Mf(r). Therefore g has order at most ρ by [F1].

F1step 1.1step 1.2algebra
3.1

Fix real numbers σ,s with ρ<σ<s. By [F1] and step 2.1, for all sufficiently large r one has logMg(2r)(2r)σ. Applying [F2] to g, whose value at 0 is nonzero by step 1.1, yields n(r)log212π02πlogg(2reit)dtlogg(0)(2r)σlogg(0), where n(r) counts the nonzero zeros of f in zr. Thus n(r)Crσ for all large r.

F1F2step 1.1step 2.1choosealgebra
4.1

Split the nonzero zeros into dyadic shells 2jan<2j+1. The number of zeros in the jth shell is at most n(2j+1), so for large j one has 2jan<2j+1ansn(2j+1)2jsC2(j+1)σ2js=C2σ2j(sσ). Since sσ>0, the dyadic majorant is summable.

step 3.1algebra
5.1

Therefore n1ans< for every s>ρ. By [F3], this means the exponent of convergence λ of the nonzero zero sequence satisfies λρ.

F3step 4.1algebra
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29Open item page →

Hadamard factorization for finite-order entire functions

Statement

Let f be a nonzero entire function of finite order ρ, let m be the order of its zero at 0, let (an)n1 list its nonzero zeros with multiplicity and without finite accumulation point, and put

p:=ρ.

Then there is a polynomial Q of degree at most p such that

f(z)=zmeQ(z)n1Ep(z/an).

In particular, a finite-order entire function factors as an exponential of a polynomial times a canonical product whose genus is bounded by its order.

Facts & Assumptions

Given: A nonzero entire function f of finite order ρ, its zero order m at 0, and its nonzero zero sequence (an).

[F1]

The order of an entire function is the limsup growth rate of loglogMf(r) (The order of an entire function).

[F2]

The exponent of convergence of the nonzero zero sequence of a finite-order entire function does not exceed the order (The exponent of convergence of the zeros of an entire function does not exceed its order).

[F3]

If an(p+1) converges, then the canonical product Ep(z/an) converges normally on C and has exactly the zeros an with their multiplicities (A canonical product converges when the (p+1)-power reciprocal sum converges).

[F4]

The elementary factor is Ep(w)=(1w)exp ⁣(w+w22++wpp), and on the unit disc it satisfies 1Ep(w)wp+1 (Weierstrass elementary factors, The unit-disc estimate for Weierstrass elementary factors).

[F5]

Every nonzero entire function factors as an exponential times a Weierstrass product over its zeros (Weierstrass factorization for entire functions).

[F6]

An entire function with polynomial growth is a polynomial (An entire function of polynomial growth is a polynomial).

[F7]

If a holomorphic function on a bounded complex domain extends continuously to the boundary, then its modulus is bounded there by a boundary value (Boundary maximum modulus principle on a bounded domain).

[F8]

If a holomorphic function has an interior local modulus maximum, then it is constant (Local maximum modulus principle).

Proof

technique · direct
1.1

Since p+1>ρ, [F2] gives n1an(p+1)<. Therefore [F3] constructs the canonical product P(z):=n1Ep(z/an), and P has exactly the nonzero zeros of f, with multiplicity.

F2F3F1givenconstruct
1.2

Fix a real number σ with ρ<σp+1. By [F1], for all sufficiently large R one has logMf(R)Rσ, and [F2] gives a finite sum Sσ:=n1anσ<.

F1F2givenchoosealgebra
2.1

The quotient H(z):=f(z)/(zmP(z)) is therefore entire and zero-free: the factor zm removes the zero at 0, and step 1.1 removes every other zero of f with the correct multiplicity.

step 1.1givenalgebra
2.2

There is a constant Aσ0 such that 1Ep(w)exp(Aσwσ) whenever w2 or w1/2. Indeed, if w2, then [F4] gives 1Ep(w)=11wexp ⁣(Re ⁣(w+w22++wpp))exp ⁣(k=1pwkk)exp(Aσwσ), because 1w1 and kp<σ+1. If w1/2, then [F4] gives 1Ep(w)wp+1wσ1/2, so 1Ep(w)111Ep(w)exp(2wσ). Enlarge the constant once to cover both cases.

F4step 1.2algebra
3.1

Fix r1 such that r is not one of the moduli an, and put H1(z):=f(z)zman2rEp(z/an),H2(z):=an>2rEp(z/an)1. Then H=H1H2. If z=4r, every factor of H1 satisfies z/an2, so steps 1.2 and 2.2 give H1(z)f(z)exp ⁣(Aσzσan2ranσ)exp((1+AσSσ)zσ) for all sufficiently large r. The function H1 is entire by step 2.1, so [F7] applies on the disc z<4r and gives the same bound for z=r. On that circle every factor of H2 satisfies z/an<1/2, so step 2.2 gives H2(z)exp ⁣(Aσzσan>2ranσ)exp(AσSσzσ). Therefore H(z)exp(Bσzσ) on z=r for all sufficiently large admissible r, with Bσ:=1+2AσSσ. Since such radii occur arbitrarily large, H has order at most ρ.

F7step 2.1step 1.2step 2.2algebra
4.1

Apply [F5] to the zero-free entire function H. Since H has no zeros at all, its Weierstrass product part is empty, so there is an entire function g with H=eg. Hence f(z)=zmeg(z)P(z).

F5step 2.1step 3.1construct
4.2

For R>0, let AR:=1+maxζ=RRe(g(ζ)g(0)). Because H=eReg and step 3.1 bounds MH(R) by exp(Cσ(1+Rσ)), one has ARCσ(1+Rσ). On the disc z<R, define FR(z):=(g(z)g(0))/(2AR(g(z)g(0))). If z=R, then Re(g(z)g(0))AR1, so 2AR(g(z)g(0))2g(z)g(0)2=4AR(ARRe(g(z)g(0)))>0, hence FR(z)<1 on the boundary circle. Also FR(0)=0, so FR(z)/z extends holomorphically across 0. If FR(z)/z had an interior local maximum larger than 1/R, then multiplying by the constant R would give an interior local modulus maximum for a nonconstant holomorphic function, contradicting [F8]. Therefore FR(z)z/R for z<R.

F8step 3.1constructalgebra
5.1

For zR/2, step 4.2 gives FR(z)1/2, so g(z)g(0)=2ARFR(z)/1+FR(z)2AR. Together with the bound on AR, this yields g(z)Cσ(1+Rσ) for zR/2. Taking R:=2(1+z) gives a global growth estimate g(z)Cσ(5)(1+z)σ on C.

step 4.2algebra
6.1

Step 5.1 holds for every σ>ρ. Applying [F6] to any one such σ makes g a polynomial; because the polynomial degree is an integer and the bound is available for every σ>ρ, the degree of g is at most p=ρ. Put Q:=g. Then step 4.1 becomes f(z)=zmeQ(z)n1Ep(z/an) with degQp, exactly as claimed.

F6step 4.1step 5.1
CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

A nonintegral order bounds the canonical genus by its floor

Statement

Let f be a nonzero entire function of finite nonintegral order ρ, and let (an)n1 be its nonzero zero sequence. Then the canonical genus of (an) is at most ρ.

Facts & Assumptions

Given: A nonzero entire function f of finite nonintegral order ρ and its nonzero zero sequence (an).

[F1]

Hadamard factorization writes f as an exponential of a polynomial times the genus-ρ canonical product over its nonzero zeros (Hadamard factorization for finite-order entire functions).

Proof

technique · direct
1.1

By [F1], the genus-ρ canonical product n1Eρ(z/an) already converges.

F1given
2.1

By definition, the canonical genus is the least integer for which the corresponding canonical product converges. Step 1.1 therefore gives canonical genusρ. The nonintegrality of ρ makes ρ the largest integer strictly below ρ, which is the usual Hadamard bound.

F1step 1.1algebra

5 · Examples, counterexamples and false statements

None yet.

Sources