Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passaudited 2026-08-29
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 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

Depends on

Used by

Dependency tree · two levels

10 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