Log-derivative control for genus‑1 canonical products.

The key output is a pointwise formula for the logarithmic derivative of w ↦ ∏' i, weierstrassE 1 (w / z i) in terms of a (provably summable) partial-fraction series.

theorem Hadamard.OrderOne.weierstrass_E_one_eq_zero_iff (w : ℂ) : weierstrassE 1 w = 0 ↔ w = 1

theorem Hadamard.OrderOne.weierstrass_E_one_ne_zero (w : ℂ) (hw : w ≠ 1) : weierstrassE 1 w ≠ 0

theorem Hadamard.OrderOne.weierstrass_E_one_div_ne_zero {a x : ℂ} (ha : a ≠ 0) (hx : x ≠ a) : weierstrassE 1 (x / a) ≠ 0

theorem Hadamard.OrderOne.logDeriv_weierstrass_E_one_div {a x : ℂ} (ha : a ≠ 0) (hx : x ≠ a) : logDeriv (fun (w : ℂ) => weierstrassE 1 (w / a)) x = x / (a * (x - a))

theorem Hadamard.OrderOne.summable_logDeriv_weierstrass_E_one_div_of_summable_inv_norm_sq {ι : Type} {z : ι → ℂ} (hz0 : ∀ (i : ι), z i ≠ 0) (h : Summable fun (i : ι) => 1 / ‖z i‖ ^ 2) (x : ℂ) (hx : ∀ (i : ι), x ≠ z i) : Summable fun (i : ι) => logDeriv (fun (w : ℂ) => weierstrassE 1 (w / z i)) x

theorem Hadamard.OrderOne.weierstrass_E_div_ne_zero (p : ℕ) {a x : ℂ} (ha : a ≠ 0) (hx : x ≠ a) : weierstrassE p (x / a) ≠ 0

Rank-p version: weierstrassE p (x / a) ≠ 0 whenever a ≠ 0 and x ≠ a.

theorem Hadamard.OrderOne.tprod_weierstrass_E_div_ne_zero_of_summable_inv_norm_pow {ι : Type u_1} {z : ι → ℂ} {p : ℕ} (hz0 : ∀ (i : ι), z i ≠ 0) (h : Summable fun (i : ι) => 1 / ‖z i‖ ^ (p + 1)) (x : ℂ) (hx : ∀ (i : ι), x ≠ z i) : ∏' (i : ι), weierstrassE p (x / z i) ≠ 0

Rank-p version: the rank-p canonical product is nonzero when the evaluation point is not one of the zeros. Generalizes tprod_weierstrass_E_one_div_ne_zero_of_summable_inv_norm_sq to exponent p+1.

theorem Hadamard.OrderOne.tprod_weierstrass_E_one_div_ne_zero_of_summable_inv_norm_sq {ι : Type} {z : ι → ℂ} (hz0 : ∀ (i : ι), z i ≠ 0) (h : Summable fun (i : ι) => 1 / ‖z i‖ ^ 2) (x : ℂ) (hx : ∀ (i : ι), x ≠ z i) : ∏' (i : ι), weierstrassE 1 (x / z i) ≠ 0

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

theorem Hadamard.OrderOne.logDeriv_exp_mul_tprod_weierstrass_E_one_eq_tsum_of_summable_inv_norm_sq {ι : Type} {z : ι → ℂ} (hz0 : ∀ (i : ι), z i ≠ 0) (h : Summable fun (i : ι) => 1 / ‖z i‖ ^ 2) (x : ℂ) (hx : ∀ (i : ι), x ≠ z i) (a b : ℂ) : logDeriv (fun (w : ℂ) => Complex.exp (a * w + b) * ∏' (i : ι), weierstrassE 1 (w / z i)) x = a + ∑' (i : ι), x / (z i * (x - z i))