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.

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

Depends on

Used by

Dependency tree · two levels

11 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