Zero sets with multiplicity

ZeroSetMultiplicity refines ZeroSet with a multiplicity function, and re-indexes the zeros as a sigma type so that the factorization theorem applies without assuming simple zeros.

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

A choice of zeros for f, together with a (positive) multiplicity for each zero.

• Zero : Type
• z : self.Zero → ℂ
• isZero (ρ : self.Zero) : f (self.z ρ) = 0
• mult : self.Zero → ℕ

  Multiplicity attached to each indexed zero.

• mult_pos (ρ : self.Zero) : 0 < self.mult ρ

  Multiplicities are positive.

def Hadamard.ZeroSetMultiplicity.ZeroWithMultiplicity {f : ℂ → ℂ} (Z : ZeroSetMultiplicity f) : Type

Repeat each zero according to its multiplicity.

Equations

• Z.ZeroWithMultiplicity = ((ρ : Z.Zero) × Fin (Z.mult ρ))

def Hadamard.ZeroSetMultiplicity.zWithMultiplicity {f : ℂ → ℂ} (Z : ZeroSetMultiplicity f) : Z.ZeroWithMultiplicity → ℂ

The underlying complex value of a repeated zero index.

Equations

• Z.zWithMultiplicity i = Z.z i.fst

@[simp]

theorem Hadamard.ZeroSetMultiplicity.zWithMultiplicity_mk {f : ℂ → ℂ} (Z : ZeroSetMultiplicity f) (ρ : Z.Zero) (k : Fin (Z.mult ρ)) : Z.zWithMultiplicity ⟨ρ, k⟩ = Z.z ρ

noncomputable def Hadamard.ZeroSetMultiplicity.canonicalProductZeroSetMultiplicity {f : ℂ → ℂ} (Z : ZeroSetMultiplicity f) (s : ℂ) : ℂ

The genus‑1 canonical product where each zero occurs with its multiplicity.

Equations

• Z.canonicalProductZeroSetMultiplicity s = ∏' (i : Z.ZeroWithMultiplicity), Hadamard.weierstrassE 1 (s / Z.zWithMultiplicity i)