Summability of ∑ analyticOrderNatAt(f, ρ) / ‖ρ‖² from order-≤1 bounds

This is the multiplicity-aware analogue of Summability.lean: we weight each zero ρ by its vanishing order analyticOrderNatAt f ρ.

The key input is the Jensen/divisor bound upgraded to multiplicities (ZeroCounting.sum_zeros_multiplicity_le_of_max_one_maxModulus) and the derived O(r^(1+ε)) bound in TailEstimates.sum_multiplicity_zeros_le_rpow.

Dyadic ball finsets (no summability hypothesis)

theorem Hadamard.OrderOne.zerosBallFinite_of_entire {f : ℂ → ℂ} (hf_entire : Differentiable ℂ f) (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) (n : ℕ) : {ρ : Z.Zero | ‖Z.z ρ‖ ≤ 2 ^ n}.Finite

noncomputable def Hadamard.OrderOne.zerosBallFinsetOfEntire {f : ℂ → ℂ} (hf_entire : Differentiable ℂ f) (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) (n : ℕ) : Finset Z.Zero

The finite set of indexed zeros of an entire function in the closed disk of radius 2 ^ n.

Equations

• Hadamard.OrderOne.zerosBallFinsetOfEntire hf_entire Z h_zeros_only h_inj h_z_ne_zero n = ⋯.toFinset

@[simp]

theorem Hadamard.OrderOne.mem_zerosBallFinset_of_entire_iff {f : ℂ → ℂ} (hf_entire : Differentiable ℂ f) (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) (n : ℕ) (ρ : Z.Zero) : ρ ∈ zerosBallFinsetOfEntire hf_entire Z h_zeros_only h_inj h_z_ne_zero n ↔ ‖Z.z ρ‖ ≤ 2 ^ n

Main summability lemma

General-order summability at exponent p + 1

theorem Hadamard.OrderOne.summable_analyticOrderNatAt_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 : 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) : Summable fun (ρ : Z.Zero) => ↑(analyticOrderNatAt f (Z.z ρ)) / ‖Z.z ρ‖ ^ (⌊lam⌋₊ + 1)

Summability of ∑ ord_ρ(f) / ‖ρ‖^(p+1) from order f ≤ lam where p = ⌊lam⌋₊.

This is the general-order analogue of summable_analyticOrderNatAt_div_norm_sq_of_order_le_one: given order f ≤ lam, the multiplicity-weighted sum converges at the exponent ⌊lam⌋₊ + 1 (which is strictly greater than lam, giving a geometric decay ratio < 1).

The proof uses the weighted dyadic shell argument with:

• εcount := (p + 1 - lam) / 2 in place of εcount := 1/2, ensuring lam + εcount < p + 1 so that q := 2 ^ ((lam + εcount) - (p + 1)) is in (0, 1);
• the exponent p + 1 in place of 2;
• the generalized weighted counting bound sum_multiplicity_zeros_le_rpow_of_order_le in place of sum_multiplicity_zeros_le_rpow.

theorem Hadamard.OrderOne.summable_analyticOrderNatAt_div_norm_sq_of_order_le_one {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) : Summable fun (ρ : Z.Zero) => ↑(analyticOrderNatAt f (Z.z ρ)) / ‖Z.z ρ‖ ^ 2