Finiteness/escape-to-infinity lemmas for genus‑1 style summability hypotheses.
These are the “cheap topology” inputs used repeatedly when working with canonical products:
from summability of 1 / ‖z i‖^2 (and a nonzero hypothesis), we get that only finitely many
indices have ‖z i‖ ≤ R for any fixed R > 0.
theorem
Hadamard.OrderOne.finite_norm_le_of_summable_inv_norm_pow
{ι : Type u_1}
{z : ι → ℂ}
{p : ℕ}
(hz0 : ∀ (i : ι), z i ≠ 0)
(h : Summable fun (i : ι) => 1 / ‖z i‖ ^ (p + 1))
{R : ℝ}
(hR : 0 < R)
:
General-exponent finiteness.
The exponent ≥ 1 analogue of finite_norm_le_of_summable_inv_norm_sq:
given ∑ 1/‖z i‖^(p+1) < ∞ (for p : ℕ) and all z i ≠ 0, only finitely
many i have ‖z i‖ ≤ R.
theorem
Hadamard.OrderOne.tendsto_norm_atTop_of_summable_inv_norm_sq
{ι : Type}
{z : ι → ℂ}
(hz0 : ∀ (i : ι), z i ≠ 0)
(h : Summable fun (i : ι) => 1 / ‖z i‖ ^ 2)
:
Filter.Tendsto (fun (i : ι) => ‖z i‖) Filter.cofinite Filter.atTop