Zero sets in the unit disc (source code)

= Zero sets in the unit disc

A nonzero <holomorphic function> on the <unit disc> can have exactly a prescribed sequence of zeros, counted with <multiplicity>, if and only if that sequence is locally finite in the disc. Necessity is the <identity theorem for holomorphic functions>. For sufficiency, remove a finite number $m$ of zeros at zero and enumerate the others as $a_n$, so $|a_n|\to1$. Use the <Weierstrass elementary factors> $E_n(t)=(1-t)\exp(\sum_{j=1}^nt^j/j)$. On every <compact> subdisc, eventually $|z/a_n|\le q<1$ and $|\log E_n(z/a_n)|\le q^{n+1}/((n+1)(1-q))$. Hence $z^m\prod_nE_n(z/a_n)$ converges locally uniformly and has exactly the prescribed zeros. Finite sequences simply give finite products.