Zero counting bounds for a ZeroSet enumeration, in the order‑≤ 1 regime.

This file bridges the Jensen/divisor-based counting lemma in LZC/HadamardFactorization/ZeroCounting.lean to the ZeroSet-based canonical product development.

Relating ZeroSet enumerations to divisor support

theorem Hadamard.OrderOne.mem_divisor_support_of_simple_zero {f : ℂ → ℂ} (hf : Differentiable ℂ f) {R : ℝ} (_hR : 0 < R) {u : ℂ} (hu_mem : u ∈ Metric.closedBall 0 |R|) (hu0 : f u = 0) (hu' : deriv f u ≠ 0) : u ∈ (MeromorphicOn.divisor f (Metric.closedBall 0 |R|)).support

theorem Hadamard.OrderOne.mem_divisor_support_of_zero {f : ℂ → ℂ} (hf : Differentiable ℂ f) {R : ℝ} {u : ℂ} (hu_mem : u ∈ Metric.closedBall 0 |R|) (hf0 : f 0 ≠ 0) (hu0 : f u = 0) : u ∈ (MeromorphicOn.divisor f (Metric.closedBall 0 |R|)).support

Zero counting for the ZeroSet index type

theorem Hadamard.OrderOne.ncard_zeros_le_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) (h_simple : ∀ (ρ : Z.Zero), deriv f (Z.z ρ) ≠ 0) (ε : ℝ) : 0 < ε → ∃ (R₀ : ℝ), ∀ (r : ℝ), R₀ ≤ r → ↑{ρ : Z.Zero | ‖Z.z ρ‖ ≤ r}.ncard ≤ ((2 * r) ^ (1 + ε) - Real.log ‖f 0‖) / Real.log 2

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

General-order multiplicity-weighted zero counting.

This is the order f ≤ lam analogue of sum_multiplicity_zeros_le_of_order_le_one. The proof is identical except we use the general max-modulus growth bound maxModulus_le_exp_rpow_of_order_le instead of its order-1 specialization.

theorem Hadamard.OrderOne.sum_multiplicity_zeros_le_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) (ε : ℝ) : 0 < ε → ∃ (R₀ : ℝ), ∀ (r : ℝ), R₀ ≤ r → (∑ᶠ (ρ : Z.Zero), if ‖Z.z ρ‖ ≤ r then ↑(analyticOrderNatAt f (Z.z ρ)) else 0) ≤ ((2 * r) ^ (1 + ε) - Real.log ‖f 0‖) / Real.log 2

Multiplicity-weighted zero counting for a ZeroSet enumeration, in the order-≤ 1 regime.

This bounds ∑ ord_ρ(f) over zeros ρ with ‖Z.z ρ‖ ≤ r, where ord_ρ(f) is the vanishing order (analyticOrderNatAt f (Z.z ρ)).