Zero sets of entire functions

The ZeroSet structure packaging the zeros of an entire function together with the data the Hadamard factorization needs, and the associated canonical product.

structure Hadamard.ZeroSet (f : ℂ → ℂ) : Type 1

A choice of zeros for a function f, with explicit enumeration.

• Zero : Type

  Index type for the chosen zeros.

• z : self.Zero → ℂ

  The underlying complex value of a zero.

• isZero (ρ : self.Zero) : f (self.z ρ) = 0

  Each indexed value is a genuine zero of f.

noncomputable def Hadamard.canonicalProductZeroSet {f : ℂ → ℂ} (Z : ZeroSet f) (s : ℂ) : ℂ

The canonical genus‑1 Weierstrass product over a countable zero set.

Equations

• Hadamard.canonicalProductZeroSet Z s = ∏' (ρ : Z.Zero), Hadamard.weierstrassE 1 (s / Z.z ρ)