Local-uniform convergence (and hence holomorphy) of the genus‑1 Weierstrass product
∏' i, weierstrassE 1 (s / z i) under the standard hypothesis ∑ 1/‖z i‖² < ∞
and a nonzero condition on the z i.
theorem
Hadamard.OrderOne.hasProdLocallyUniformlyOn_weierstrass_E_of_summable_inv_norm_pow
{ι : Type u_1}
{z : ι → ℂ}
{p : ℕ}
(hz0 : ∀ (i : ι), z i ≠ 0)
(h : Summable fun (i : ι) => 1 / ‖z i‖ ^ (p + 1))
:
HasProdLocallyUniformlyOn (fun (i : ι) (w : ℂ) => weierstrassE p (w / z i))
(fun (w : ℂ) => ∏' (i : ι), weierstrassE p (w / z i)) Set.univ
Rank-p analogue of
hasProdLocallyUniformlyOn_weierstrass_E_one_of_summable_inv_norm_sq.
theorem
Hadamard.OrderOne.differentiableOn_tprod_weierstrass_E_of_summable_inv_norm_pow
{ι : Type u_1}
{z : ι → ℂ}
{p : ℕ}
(hz0 : ∀ (i : ι), z i ≠ 0)
(h : Summable fun (i : ι) => 1 / ‖z i‖ ^ (p + 1))
:
DifferentiableOn ℂ (fun (w : ℂ) => ∏' (i : ι), weierstrassE p (w / z i)) Set.univ
Rank-p analogue of differentiableOn_tprod_weierstrass_E_one_of_summable_inv_norm_sq.
theorem
Hadamard.OrderOne.differentiable_tprod_weierstrass_E_of_summable_inv_norm_pow
{ι : Type u_1}
{z : ι → ℂ}
{p : ℕ}
(hz0 : ∀ (i : ι), z i ≠ 0)
(h : Summable fun (i : ι) => 1 / ‖z i‖ ^ (p + 1))
:
Differentiable ℂ fun (w : ℂ) => ∏' (i : ι), weierstrassE p (w / z i)
Entire rank-p canonical product. The Differentiable (globally) form.
theorem
Hadamard.OrderOne.hasProdLocallyUniformlyOn_weierstrass_E_one_of_summable_inv_norm_sq
{ι : Type}
{z : ι → ℂ}
(hz0 : ∀ (i : ι), z i ≠ 0)
(h : Summable fun (i : ι) => 1 / ‖z i‖ ^ 2)
:
HasProdLocallyUniformlyOn (fun (i : ι) (w : ℂ) => weierstrassE 1 (w / z i))
(fun (w : ℂ) => ∏' (i : ι), weierstrassE 1 (w / z i)) Set.univ