Dyadic ball finsets under ∑ 1/‖z ρ‖² < ∞

theorem Hadamard.OrderOne.zerosBallFinite {f : ℂ → ℂ} (Z : ZeroSet f) (h_z_ne_zero : ∀ (ρ : Z.Zero), Z.z ρ ≠ 0) (h_summable : Summable fun (ρ : Z.Zero) => 1 / ‖Z.z ρ‖ ^ 2) (n : ℕ) : {ρ : Z.Zero | ‖Z.z ρ‖ ≤ 2 ^ n}.Finite

The finite set of indices with ‖Z.z ρ‖ ≤ 2^n.

noncomputable def Hadamard.OrderOne.zerosBallFinset {f : ℂ → ℂ} (Z : ZeroSet f) (h_z_ne_zero : ∀ (ρ : Z.Zero), Z.z ρ ≠ 0) (h_summable : Summable fun (ρ : Z.Zero) => 1 / ‖Z.z ρ‖ ^ 2) (n : ℕ) : Finset Z.Zero

The set of indices with ‖Z.z ρ‖ ≤ 2^n, as a Finset.

Equations

• Hadamard.OrderOne.zerosBallFinset Z h_z_ne_zero h_summable n = ⋯.toFinset

@[simp]

theorem Hadamard.OrderOne.mem_zerosBallFinset_iff {f : ℂ → ℂ} (Z : ZeroSet f) (h_z_ne_zero : ∀ (ρ : Z.Zero), Z.z ρ ≠ 0) (h_summable : Summable fun (ρ : Z.Zero) => 1 / ‖Z.z ρ‖ ^ 2) (n : ℕ) (ρ : Z.Zero) : ρ ∈ zerosBallFinset Z h_z_ne_zero h_summable n ↔ ‖Z.z ρ‖ ≤ 2 ^ n

@[simp]

theorem Hadamard.OrderOne.card_zerosBallFinset {f : ℂ → ℂ} (Z : ZeroSet f) (h_z_ne_zero : ∀ (ρ : Z.Zero), Z.z ρ ≠ 0) (h_summable : Summable fun (ρ : Z.Zero) => 1 / ‖Z.z ρ‖ ^ 2) (n : ℕ) : (zerosBallFinset Z h_z_ne_zero h_summable n).card = {ρ : Z.Zero | ‖Z.z ρ‖ ≤ 2 ^ n}.ncard

Tail estimates for genus‑1 canonical products (order‑≤1 regime).

This module will eventually house the dyadic-shell bounds (Conway XI §1–2) used in the growth analysis. For now, we start by packaging a convenient O(r^(1+ε)) bound for the zero-counting function coming from ZeroCountingBounds.

theorem Hadamard.OrderOne.ncard_zeros_le_rpow {f : ℂ → ℂ} (hf_entire : Differentiable ℂ f) (hf_finite : hasFiniteOrder f) (hf_order_le : order f ≤ 1) (Z : ZeroSet 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_simple : ∀ (ρ : Z.Zero), deriv f (Z.z ρ) ≠ 0) (ε : ℝ) : 0 < ε → ∃ (R₀ : ℝ) (C : ℝ), 0 ≤ C ∧ ∀ (r : ℝ), R₀ ≤ r → ↑{ρ : Z.Zero | ‖Z.z ρ‖ ≤ r}.ncard ≤ C * r ^ (1 + ε)

theorem Hadamard.OrderOne.sum_multiplicity_zeros_le_rpow_of_order_le {f : ℂ → ℂ} (hf_entire : Differentiable ℂ f) (hf_finite : hasFiniteOrder f) {lam : ℝ} (hf_order_le : order f ≤ lam) (hlam_nonneg : 0 ≤ lam) (Z : ZeroSet 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) (ε : ℝ) : 0 < ε → ∃ (R₀ : ℝ) (C : ℝ), 0 ≤ C ∧ ∀ (r : ℝ), R₀ ≤ r → (∑ᶠ (ρ : Z.Zero), if ‖Z.z ρ‖ ≤ r then ↑(analyticOrderNatAt f (Z.z ρ)) else 0) ≤ C * r ^ (lam + ε)

General-order multiplicity-weighted zero counting, clean form.

The order f ≤ lam analogue of sum_multiplicity_zeros_le_rpow, giving a constant bound of the form C * r ^ (lam + ε) for r large. Obtained by composing the general-order Jensen bound with a rewrite to absorb the log ‖f 0‖ term.

This is Step 1 of tmp-conway/HadamardGeneral.lean (used to derive summability of ∑ mult(ρ) / ‖ρ‖^(p+1) under order ≤ lam).

theorem Hadamard.OrderOne.sum_multiplicity_zeros_le_rpow {f : ℂ → ℂ} (hf_entire : Differentiable ℂ f) (hf_finite : hasFiniteOrder f) (hf_order_le : order f ≤ 1) (Z : ZeroSet 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) (ε : ℝ) : 0 < ε → ∃ (R₀ : ℝ) (C : ℝ), 0 ≤ C ∧ ∀ (r : ℝ), R₀ ≤ r → (∑ᶠ (ρ : Z.Zero), if ‖Z.z ρ‖ ≤ r then ↑(analyticOrderNatAt f (Z.z ρ)) else 0) ≤ C * r ^ (1 + ε)

theorem Hadamard.OrderOne.sum_invNorm_le_rpow_of_two_pow {f : ℂ → ℂ} (hf_entire : Differentiable ℂ f) (hf_finite : hasFiniteOrder f) (hf_order_le : order f ≤ 1) (Z : ZeroSet 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_simple : ∀ (ρ : Z.Zero), deriv f (Z.z ρ) ≠ 0) (h_summable : Summable fun (ρ : Z.Zero) => 1 / ‖Z.z ρ‖ ^ 2) (ε : ℝ) : 0 < ε → ∃ (n₀ : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), n₀ ≤ n → ∑ ρ ∈ zerosBallFinset Z h_z_ne_zero h_summable n, 1 / ‖Z.z ρ‖ ≤ C * (2 ^ n) ^ ε

Dyadic tail decay for ∑ 1/‖Z.z ρ‖²

theorem Hadamard.OrderOne.tsum_invNorm_sq_tail_le_rpow_of_two_pow {f : ℂ → ℂ} (hf_entire : Differentiable ℂ f) (hf_finite : hasFiniteOrder f) (hf_order_le : order f ≤ 1) (Z : ZeroSet 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_simple : ∀ (ρ : Z.Zero), deriv f (Z.z ρ) ≠ 0) (h_summable : Summable fun (ρ : Z.Zero) => 1 / ‖Z.z ρ‖ ^ 2) (ε : ℝ) : 0 < ε → ε < 1 → ∃ (n₀ : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), n₀ ≤ n → ∑' (ρ : ↑{ρ : Z.Zero | 2 ^ (n + 1) < ‖Z.z ρ‖}), 1 / ‖Z.z ↑ρ‖ ^ 2 ≤ C * (2 ^ n) ^ (ε - 1)