Multiplicity-aware log-derivative formulas for genus‑1 canonical products.

We model multiplicity by repeating each zero index i exactly m i times via the sigma type Σ i, Fin (m i). This keeps the analytic infrastructure unchanged, and the resulting log-derivative series carries the expected multiplicity coefficient.

@[reducible, inline]

abbrev Hadamard.OrderOne.WithMultiplicity (ι : Type) (m : ι → ℕ) : Type

Duplicate each index i exactly m i times.

Equations

• Hadamard.OrderOne.WithMultiplicity ι m = ((i : ι) × Fin (m i))

theorem Hadamard.OrderOne.logDeriv_tprod_weierstrass_E_one_eq_tsum_of_summable_mul_inv_norm_sq {ι : Type} {z : ι → ℂ} {m : ι → ℕ} (hz0 : ∀ (i : ι), z i ≠ 0) (h : Summable fun (i : ι) => ↑(m i) / ‖z i‖ ^ 2) (x : ℂ) (hx : ∀ (i : ι), x ≠ z i) : logDeriv (fun (w : ℂ) => ∏' (j : WithMultiplicity ι m), weierstrassE 1 (w / z j.fst)) x = ∑' (i : ι), ↑(m i) * (x / (z i * (x - z i)))