Zero counting bounds from Jensen's formula.

This module packages one very specific estimate we use repeatedly: if order f ≤ 1, then the number of (distinct) zeros in a disk grows like O(r^(1+ε)).

We express “distinct zeros” using the MeromorphicOn.divisor support on a closed ball; for an analytic function this support is exactly the set of zeros in the ball (no poles).

From order ≤ 1 to a crude maxModulus upper bound

theorem Hadamard.ZeroCounting.maxModulus_le_exp_rpow_of_order_le (f : ℂ → ℂ) (hf_finite : hasFiniteOrder f) {lam : ℝ} (hf_order_le : order f ≤ lam) (ε : ℝ) : 0 < ε → ∃ (R₀ : ℝ), ∀ (r : ℝ), R₀ ≤ r → maxModulus f r ≤ Real.exp (r ^ (lam + ε))

General-order max-modulus growth bound.

If f has finite order with order f ≤ lam, then for every ε > 0 there is R₀ such that for all r ≥ R₀, maxModulus f r ≤ Real.exp (r ^ (lam + ε)).

This is the order ≤ lam analogue of maxModulus_le_exp_rpow_of_order_le_one. The proof is exactly the same: the specific constant 1 in the latter never interacts with the analysis, it is simply the bound on the limsup.

theorem Hadamard.ZeroCounting.maxModulus_le_exp_rpow_of_order_le_one (f : ℂ → ℂ) (hf_finite : hasFiniteOrder f) (hf_order_le : order f ≤ 1) (ε : ℝ) : 0 < ε → ∃ (R₀ : ℝ), ∀ (r : ℝ), R₀ ≤ r → maxModulus f r ≤ Real.exp (r ^ (1 + ε))

Jensen ⇒ a bound on the number of zeros

Variant: avoid the 1 ≤ maxModulus f R side condition

The lemma card_zeros_le_of_maxModulus assumes 1 ≤ maxModulus f R in order to compare the circle-average of log ‖f‖ with log (maxModulus f R) even at points where f vanishes on the circle (since Real.log 0 = 0).

For growth applications we want an unconditional bound, so we instead compare with log (max 1 (maxModulus f R)).

theorem Hadamard.ZeroCounting.card_zeros_le_of_max_one_maxModulus (f : ℂ → ℂ) {R : ℝ} (hR : 0 < R) (hf_entire : Differentiable ℂ f) (hf0 : f 0 ≠ 0) : ↑{u : ℂ | u ∈ (MeromorphicOn.divisor f (Metric.closedBall 0 |R|)).support ∧ ‖u‖ ≤ R / 2}.ncard ≤ (Real.log (max 1 (maxModulus f R)) - Real.log ‖f 0‖) / Real.log 2

Jensen ⇒ a bound on the sum of multiplicities (divisor weights)

The previous lemmas bound the number of distinct zeros in a disk by discarding multiplicities. For multiplicity-aware Hadamard products we instead need control of ∑ multiplicity(u) over zeros u in a disk.

We express this as the sum of divisor values on the same set: for analytic functions the divisor value at u is exactly the vanishing multiplicity of f at u.

theorem Hadamard.ZeroCounting.card_zeros_le_of_maxModulus (f : ℂ → ℂ) {R : ℝ} (hR : 0 < R) (hf_entire : Differentiable ℂ f) (hf0 : f 0 ≠ 0) (hM : 1 ≤ maxModulus f R) : ↑{u : ℂ | u ∈ (MeromorphicOn.divisor f (Metric.closedBall 0 |R|)).support ∧ ‖u‖ ≤ R / 2}.ncard ≤ (Real.log (maxModulus f R) - Real.log ‖f 0‖) / Real.log 2

theorem Hadamard.ZeroCounting.sum_zeros_multiplicity_le_of_max_one_maxModulus (f : ℂ → ℂ) {R : ℝ} (hR : 0 < R) (hf_entire : Differentiable ℂ f) (hf0 : f 0 ≠ 0) : (∑ᶠ (u : ℂ), if ‖u‖ ≤ R / 2 then ↑((MeromorphicOn.divisor f (Metric.closedBall 0 |R|)) u) else 0) ≤ (Real.log (max 1 (maxModulus f R)) - Real.log ‖f 0‖) / Real.log 2

Jensen-style bound on the sum of divisor weights in the disk ‖u‖ ≤ R/2.

This is the multiplicity-aware analogue of card_zeros_le_of_max_one_maxModulus.

The LHS is ∑_{u : ‖u‖ ≤ R/2} ord_u(f) where ord_u(f) is the (nonnegative) divisor value.