Step 0. Preliminaries

0.1 Rank-p canonical product for a ZeroSetMultiplicity

Hadamard.ZeroSetMultiplicity.canonicalProductZeroSetMultiplicity is currently hard-coded to weierstrassE 1. The general theorem needs the rank-p variant. We introduce it here so downstream lemmas can refer to it; the genus-1 version is a special case.

noncomputable def Hadamard.General.canonicalProductZeroSetMultiplicityRank {f : ℂ → ℂ} (Z : ZeroSetMultiplicity f) (p : ℕ) (s : ℂ) : ℂ

The rank-p canonical Weierstrass product over a ZeroSetMultiplicity, with each zero repeated according to its multiplicity.

Equations

• Hadamard.General.canonicalProductZeroSetMultiplicityRank Z p s = ∏' (i : Z.ZeroWithMultiplicity), Hadamard.weierstrassE p (s / Z.zWithMultiplicity i)

@[simp]

theorem Hadamard.General.canonicalProductZeroSetMultiplicityRank_one {f : ℂ → ℂ} (Z : ZeroSetMultiplicity f) (s : ℂ) : canonicalProductZeroSetMultiplicityRank Z 1 s = Z.canonicalProductZeroSetMultiplicity s

Step 1. Summability at exponent p + 1

Target. If f is entire of order ≤ λ, p = ⌊λ⌋₊, and the zeros of f are enumerated by Z : ZeroSetMultiplicity f with distinct non-zero values, then the weighted sum ∑ (Z.mult ρ) / ‖Z.z ρ‖^(p+1) converges.

Existing infrastructure:

• Hadamard.OrderOne.summable_analyticOrderNatAt_div_norm_sq_of_order_le_one gives this at p = 1 (exponent 2), using analyticOrderNatAt as the multiplicity function. We generalize the exponent from 2 to p+1.

LaTeX: the proof goes via Jensen-type zero counting. If $n(r) \le r^{\lambda + \varepsilon}$ (standard, from the max-modulus bound and Jensen's formula), then $\sum_n |a_n|^{-(p+1)}$ converges by a dyadic decomposition with geometric ratio $2^{\lambda + \varepsilon - (p+1)} < 1$ since $\lambda + \varepsilon < p + 1$ for small enough $\varepsilon$ (as $p = \lfloor \lambda \rfloor$).

theorem Hadamard.General.summable_mult_div_norm_pow_of_order_le {f : ℂ → ℂ} (hf_entire : Differentiable ℂ f) (hf_finite : hasFiniteOrder f) {lam : ℝ} (hlam_nonneg : 0 ≤ lam) (hf_order_le : order f ≤ lam) (Z : ZeroSetMultiplicity f) (h_zeros_only : ∀ (s : ℂ), f s = 0 ↔ ∃ (ρ : Z.Zero), s = Z.z ρ) (h_inj : Function.Injective Z.z) (h_z_ne_zero : ∀ (ρ : Z.Zero), Z.z ρ ≠ 0) (h_mult : ∀ (ρ : Z.Zero), analyticOrderNatAt f (Z.z ρ) = Z.mult ρ) : Summable fun (ρ : Z.Zero) => ↑(Z.mult ρ) / ‖Z.z ρ‖ ^ (⌊lam⌋₊ + 1)

Step 1: Summability at exponent p+1 from order f ≤ lam with p = ⌊lam⌋₊.

Thin wrapper around the library lemma Hadamard.OrderOne.summable_analyticOrderNatAt_div_norm_pow_of_order_le that converts from analyticOrderNatAt f weights to Z.mult weights via h_mult.

Step 2. Canonical product convergence and zero structure

Target. With the summability from Step 1, the rank-p canonical product P(z) := ∏ E_p(z/Z.z ρ)^{mult ρ} converges locally uniformly on ℂ. So P is entire, and analyticOrderNatAt P (Z.z ρ) = Z.mult ρ at each zero, and P(z) = 0 ↔ ∃ ρ, z = Z.z ρ.

Existing infrastructure:

• Hadamard.OrderOne.MultipliableFactors.lean, Hadamard.OrderOne.LocallyUniformProduct.lean give the rank-1 case.

LaTeX: $|E_p(w) - 1| \le |w|^{p+1}$ for $|w| \le 1/2$ (standard). Hence on a compact disk $|z| \le R$, summing $|E_p(z/a_n)^{m_n} - 1| \le C\,(R/|a_n|)^{p+1} \cdot m_n$ for $|a_n| \ge 2R$ and applying the M-test yields local uniform convergence.

theorem Hadamard.General.summable_inv_norm_pow_zWithMultiplicity {f : ℂ → ℂ} (Z : ZeroSetMultiplicity f) {p : ℕ} (hsum : Summable fun (ρ : Z.Zero) => ↑(Z.mult ρ) / ‖Z.z ρ‖ ^ (p + 1)) : Summable fun (i : Z.ZeroWithMultiplicity) => 1 / ‖Z.zWithMultiplicity i‖ ^ (p + 1)

Summability of 1/‖zWithMultiplicity i‖^(p+1) over the sigma index type.

This is the bridge between the multiplicity-weighted summability hypothesis Summable (fun ρ : Z.Zero => (Z.mult ρ : ℝ) / ‖Z.z ρ‖ ^ (p + 1)) (weighted over distinct zeros) and the library-level hypothesis Summable (fun i : Z.ZeroWithMultiplicity => 1 / ‖Z.zWithMultiplicity i‖ ^ (p + 1)) (over the repeating sigma index).

theorem Hadamard.General.canonicalProductZeroSetMultiplicityRank_differentiable {f : ℂ → ℂ} (Z : ZeroSetMultiplicity f) {p : ℕ} (hsum : Summable fun (ρ : Z.Zero) => ↑(Z.mult ρ) / ‖Z.z ρ‖ ^ (p + 1)) (h_z_ne_zero : ∀ (ρ : Z.Zero), Z.z ρ ≠ 0) : Differentiable ℂ (canonicalProductZeroSetMultiplicityRank Z p)

Rank-p canonical product is entire.

theorem Hadamard.General.canonicalProductZeroSetMultiplicityRank_eq_zero_iff {f : ℂ → ℂ} (Z : ZeroSetMultiplicity f) {p : ℕ} (hsum : Summable fun (ρ : Z.Zero) => ↑(Z.mult ρ) / ‖Z.z ρ‖ ^ (p + 1)) (h_inj : Function.Injective Z.z) (h_z_ne_zero : ∀ (ρ : Z.Zero), Z.z ρ ≠ 0) (s : ℂ) : canonicalProductZeroSetMultiplicityRank Z p s = 0 ↔ ∃ (ρ : Z.Zero), s = Z.z ρ

The canonical product vanishes exactly on the zero set.

theorem Hadamard.General.tprod_sigma_weierstrass_E_eq_tprod_pow_generic {ι : Type} {z : ι → ℂ} {m : ι → ℕ} {p : ℕ} (hz0 : ∀ (i : ι), z i ≠ 0) (hsum : Summable fun (i : ι) => ↑(m i) / ‖z i‖ ^ (p + 1)) (s : ℂ) : ∏' (j : (i : ι) × Fin (m i)), weierstrassE p (s / z j.fst) = ∏' (i : ι), weierstrassE p (s / z i) ^ m i

Generic sigma tprod reindexing for the Weierstrass product.

General type-theoretic version: given an index type ι, a family z : ι → ℂ of nonzero points, a multiplicity function m : ι → ℕ, and summability of the weighted inverse power, the sigma tprod over Σ i, Fin (m i) equals the iterated power form ∏' i, E_p(s/z i)^(m i).

Elaboration note. Using hmul.tprod_sigma directly triggers a whnf timeout from typeclass resolution exploring instance candidates. We work around this by passing the inner multipliability explicitly via Multipliable.tprod_sigma', which bypasses the automatic sigma_factor derivation.

Preliminaries: pointwise analytic order of a single Weierstrass factor

E_p(s / Z.z ρ) has a simple zero at s = Z.z ρ. Concretely, the substitution s ↦ s / Z.z ρ is a linear map with derivative 1/Z.z ρ ≠ 0 sending Z.z ρ to 1, and E_p has analytic order 1 at 1, so the composition has analytic order 1 at Z.z ρ.

theorem Hadamard.General.analyticOrderNatAt_weierstrass_E_div {p : ℕ} {a : ℂ} (ha : a ≠ 0) : analyticOrderNatAt (fun (s : ℂ) => weierstrassE p (s / a)) a = 1

E_p(s / a) has analyticOrderNatAt equal to 1 at s = a (a ≠ 0).

theorem Hadamard.General.canonicalProductZeroSetMultiplicityRank_eq_tprod_pow {f : ℂ → ℂ} (Z : ZeroSetMultiplicity f) {p : ℕ} (hsum : Summable fun (ρ : Z.Zero) => ↑(Z.mult ρ) / ‖Z.z ρ‖ ^ (p + 1)) (h_z_ne_zero : ∀ (ρ : Z.Zero), Z.z ρ ≠ 0) (s : ℂ) : canonicalProductZeroSetMultiplicityRank Z p s = ∏' (ρ : Z.Zero), weierstrassE p (s / Z.z ρ) ^ Z.mult ρ

Power-form rewrite of the canonical product.

Specialization of tprod_sigma_weierstrass_E_eq_tprod_pow_generic to a ZeroSetMultiplicity. Provides the textbook form P(s) = ∏' ρ, E_p(s/Z.z ρ)^(Z.mult ρ).

theorem Hadamard.General.multipliable_pow_weierstrass_E_div_generic {ι : Type} {z : ι → ℂ} {m : ι → ℕ} {p : ℕ} (hz0 : ∀ (i : ι), z i ≠ 0) (hsum : Summable fun (i : ι) => ↑(m i) / ‖z i‖ ^ (p + 1)) (s : ℂ) : Multipliable fun (i : ι) => weierstrassE p (s / z i) ^ m i

Generic multipliability of the iterated power form.

theorem Hadamard.General.tprod_pow_weierstrass_E_div_ne_zero_generic {ι : Type} {z : ι → ℂ} {m : ι → ℕ} {p : ℕ} (hz0 : ∀ (i : ι), z i ≠ 0) (hsum : Summable fun (i : ι) => ↑(m i) / ‖z i‖ ^ (p + 1)) (x : ℂ) (hx : ∀ (i : ι), x ≠ z i) : ∏' (i : ι), weierstrassE p (x / z i) ^ m i ≠ 0

Generic non-vanishing of the iterated power form.

theorem Hadamard.General.multipliable_pow_weierstrass_E_div_of_summable {f : ℂ → ℂ} (Z : ZeroSetMultiplicity f) {p : ℕ} (hsum : Summable fun (ρ : Z.Zero) => ↑(Z.mult ρ) / ‖Z.z ρ‖ ^ (p + 1)) (h_z_ne_zero : ∀ (ρ : Z.Zero), Z.z ρ ≠ 0) (s : ℂ) : Multipliable fun (ρ : Z.Zero) => weierstrassE p (s / Z.z ρ) ^ Z.mult ρ

ZeroSetMultiplicity wrapper for multipliable_pow_weierstrass_E_div_generic.

noncomputable def Hadamard.General.sigmaFiberSplitEquiv {ι : Type} [DecidableEq ι] {m : ι → ℕ} (b : ι) : (i : ι) × Fin (m i) ≃ Fin (m b) ⊕ (i : { i : ι // i ≠ b }) × Fin (m ↑i)

Decompose Σ i : ι, Fin (m i) into the fiber over b and the rest.

Equations

• One or more equations did not get rendered due to their size.

theorem Hadamard.General.tprod_pow_weierstrass_E_split_generic {ι : Type} {z : ι → ℂ} {m : ι → ℕ} {p : ℕ} (hz0 : ∀ (i : ι), z i ≠ 0) (hsum : Summable fun (i : ι) => ↑(m i) / ‖z i‖ ^ (p + 1)) (b : ι) (s : ℂ) : ∏' (i : ι), weierstrassE p (s / z i) ^ m i = weierstrassE p (s / z b) ^ m b * ∏' (i : { i : ι // i ≠ b }), weierstrassE p (s / z ↑i) ^ m ↑i

Splitting lemma for the power-form Weierstrass product.

Split off the factor at index b, expressing the rest as a subtype tprod. Proved via Equiv.tprod_eq plus sigma decomposition, avoiding all typeclass-explosive Multipliable.* operations.

theorem Hadamard.General.analyticOrderNatAt_canonicalProductZeroSetMultiplicityRank {f : ℂ → ℂ} (Z : ZeroSetMultiplicity f) {p : ℕ} (hsum : Summable fun (ρ : Z.Zero) => ↑(Z.mult ρ) / ‖Z.z ρ‖ ^ (p + 1)) (h_inj : Function.Injective Z.z) (h_z_ne_zero : ∀ (ρ : Z.Zero), Z.z ρ ≠ 0) (ρ : Z.Zero) : analyticOrderNatAt (canonicalProductZeroSetMultiplicityRank Z p) (Z.z ρ) = Z.mult ρ

Multiplicity of the canonical product at each zero matches the prescribed multiplicity.

Proof:

1. Rewrite to the power form P(s) = ∏' ρ', E_p(s/Z.z ρ')^(Z.mult ρ').
2. Split off the factor at ρ via Multipliable.tprod_subtype_mul_tprod_subtype_compl: P(s) = E_p(s/Z.z ρ)^(Z.mult ρ) · Q(s) where Q is the complementary product over {ρ' : Z.Zero // ρ' ≠ ρ}.
3. Compute the order at Z.z ρ of the first factor via analyticOrderAt_pow and analyticOrderNatAt_weierstrass_E_div.
4. Show Q(Z.z ρ) ≠ 0 via the generic non-vanishing lemma applied to the subtype.
5. Combine using analyticOrderNatAt_mul.

Step 3. The quotient Q := f / (z^m · P) is entire and nowhere zero

Target. Let m := analyticOrderNatAt f 0 be the multiplicity of the zero of f at the origin (possibly 0). Define Q(z) := f(z) / (z^m · P(z)) as an update-patched function at each a_n and at 0. Then Q is entire and never vanishes.

Existing infrastructure:

• Hadamard.OrderOne.QuotientCancellation.exists_analyticAt_update_div_of_analyticOrderNatAt_eq is the pointwise ingredient (removable singularity at a common zero).
• Hadamard.OrderOne.Factorization.quotient_entire handles the rank-1 simple-zero global assembly; we generalize to rank-p + multiplicity.

We package Q as a single entire function Q : ℂ → ℂ with hQ_entire : Differentiable ℂ Q, hQ_ne : ∀ z, Q z ≠ 0, and a factorization identity hfact : ∀ z, f z = z^m · (P z) · Q z.

theorem Hadamard.General.exists_quotient_entire {f : ℂ → ℂ} (hf_entire : Differentiable ℂ f) (Z : ZeroSetMultiplicity f) {p : ℕ} (hsum : Summable fun (ρ : Z.Zero) => ↑(Z.mult ρ) / ‖Z.z ρ‖ ^ (p + 1)) (h_zeros_only : ∀ (s : ℂ), f s = 0 ↔ ∃ (ρ : Z.Zero), s = Z.z ρ) (h_inj : Function.Injective Z.z) (h_z_ne_zero : ∀ (ρ : Z.Zero), Z.z ρ ≠ 0) (h_mult : ∀ (ρ : Z.Zero), analyticOrderNatAt f (Z.z ρ) = Z.mult ρ) : ∃ (Q : ℂ → ℂ), Differentiable ℂ Q ∧ (∀ (z : ℂ), Q z ≠ 0) ∧ ∀ (z : ℂ), f z = canonicalProductZeroSetMultiplicityRank Z p z * Q z

Existence of the entire nowhere-zero quotient Q = f / P.

This is the strict form assuming f 0 ≠ 0 (equivalently, analyticOrderNatAt f 0 = 0). A wrapper that handles the zero-at-origin case by pre-processing f(z) / z^m should be added later (Conway p.289 reduction).

Steps 4–7. Collapsed: use entire_no_zeros_is_exp_polynomial directly.

Rather than building an entire logarithm g of Q, applying growth bounds, Borel–Carathéodory, and Cauchy estimates separately (classical route), we invoke the prepackaged library theorem entire_no_zeros_is_exp_polynomial (Hadamard/Basic.lean:2750), which already handles all of:

• the entire logarithm of an entire nowhere-zero function,
• the growth bound on its real part,
• the Borel–Carathéodory upgrade,
• the Cauchy coefficient estimate and polynomial extraction.

The remaining ingredient is Step 3': order Q ≤ lam. With Q = f / P both entire (and P having controlled below-bound), the growth of Q on circles is at most the growth of f times the reciprocal of the P lower bound. This is the only remaining analytic content.

We package Step 3' as the separate theorem order_Q_le_lam_of_factorization_and_order_f below.

theorem Hadamard.General.order_Q_le_lam_of_factorization {f Q : ℂ → ℂ} (hf_entire : Differentiable ℂ f) (hf_finite : hasFiniteOrder f) {lam : ℝ} (hlam : 0 ≤ lam) (hf_order_le : order f ≤ lam) (hQ_entire : Differentiable ℂ Q) (hQ_ne : ∀ (z : ℂ), Q z ≠ 0) (Z : ZeroSetMultiplicity f) {p : ℕ} (hp : p = ⌊lam⌋₊) (h_z_ne_zero : ∀ (ρ : Z.Zero), Z.z ρ ≠ 0) (h_inj : Function.Injective Z.z) (hsum : Summable fun (ρ : Z.Zero) => ↑(Z.mult ρ) / ‖Z.z ρ‖ ^ (p + 1)) (h_mult : ∀ (ρ : Z.Zero), analyticOrderNatAt f (Z.z ρ) = Z.mult ρ) (hfact : ∀ (z : ℂ), f z = canonicalProductZeroSetMultiplicityRank Z p z * Q z) : hasFiniteOrder Q ∧ order Q ≤ lam

Order bound on the quotient.

Given f = P · Q with Q entire and nowhere zero, if order f ≤ lam and the canonical product P has the standard rank-p lower bound, then order Q ≤ lam. This combines the finite-order bound on f with the Weierstrass-product lower bound to extract a polynomial growth bound on log ‖Q‖, which is exactly order Q ≤ lam.

Mathematical subtlety. A crude lower bound on ‖P(z)‖ gives log ‖P(z)‖ ≥ -C r^{p+1+ε} (from the rank-p Weierstrass lower bound log|E_p(w)| ≥ -C|w|^{p+1} applied to all factors). Since p+1 > lam, this only yields order Q ≤ p+1, one higher than needed.

The proof below uses an alternative zero-avoiding-circles argument. Zero counting and a finite pigeonhole argument choose, for every sufficiently large r, a radius R ∈ [r, 2r] separated from the zero norms. Splitting the canonical product into near and far factors gives its lower bound on that circle. Monotonicity of the maximum modulus then bounds Q at every large radius, and the growth characterization of order gives the conclusion.

For comparison, Ahlfors, Complex Analysis, third edition, Chapter 5, §3.2, pp. 210–211, proves the polynomial-degree step using differentiated Poisson–Jensen. That is a different proof from the circle argument formalized here.

Hadamard factorization for a function nonzero at the origin

The following declaration proves the f 0 ≠ 0 case of Conway, Chapter XI, Theorem 3.4 (pages 289–290). The hypotheses h_zeros_only and h_z_ne_zero force this restriction: all zeros are enumerated by Z, and every enumerated zero is nonzero. Conway handles a zero of multiplicity m at the origin by first dividing out z^m; that reduction is not part of this declaration. Multiplicities of the nonzero zeros are recorded by ZeroSetMultiplicity.

theorem Hadamard.General.hadamard_factorization_general (f : ℂ → ℂ) (hf_entire : Differentiable ℂ f) (hf_finite : hasFiniteOrder f) {lam : ℝ} (hlam : 0 ≤ lam) (hf_order_le : order f ≤ lam) (Z : ZeroSetMultiplicity f) (h_zeros_only : ∀ (s : ℂ), f s = 0 ↔ ∃ (ρ : Z.Zero), s = Z.z ρ) (h_inj : Function.Injective Z.z) (h_z_ne_zero : ∀ (ρ : Z.Zero), Z.z ρ ≠ 0) (h_mult : ∀ (ρ : Z.Zero), analyticOrderNatAt f (Z.z ρ) = Z.mult ρ) : ∃ (g : Polynomial ℂ), g.natDegree ≤ ⌊lam⌋₊ ∧ ∀ (z : ℂ), f z = Complex.exp (Polynomial.eval z g) * canonicalProductZeroSetMultiplicityRank Z ⌊lam⌋₊ z

Hadamard factorization of general finite order, in the f 0 ≠ 0 case.

For an entire function of order at most lam ≥ 0, let Z enumerate all its zeros, with their multiplicities, and assume every enumerated zero is nonzero. There is a polynomial g of degree at most ⌊lam⌋ such that

f z = Complex.exp (g.eval z) * canonicalProductZeroSetMultiplicityRank Z (Nat.floor lam) z.

The assumptions imply f 0 ≠ 0, so the formula has no factor for an origin zero. This is the corresponding special case of Conway, Chapter XI, Theorem 3.4 (page 289), with a multiplicity-indexed product. The proof combines Borel–Carathéodory, growth bounds, and Cauchy's estimate.