The zero count of a holomorphic function on a disc

The zero count of f on an open disc is the finitely supported sum ∑ᶠ z ∈ ball c R, analyticOrderNatAt f z. It is what the argument principle produces — through TauCeti.Contour.argumentPrinciple_divisor and the bridge TauCeti.Contour.divisor_eq_analyticOrderNatAt — and what Rouché's theorem (TauCeti.rouche_symm) and Hurwitz's theorem (TauCeti.hurwitz) compare. This file collects the three facts about that sum which those consumers need, none of which mentions either theorem.

Care is needed about points of infinite order, where f vanishes identically nearby: analyticOrderNatAt reads 0 there, exactly as it does where f does not vanish at all, so the count does not see such a point. That is why detecting a zero from a vanishing count (TauCeti.finsum_analyticOrderNatAt_ball_eq_zero_iff) needs a hypothesis ruling infinite order out. One point of the closed disc at which f is nonzero is enough: the disc is convex, hence preconnected, so AnalyticOnNhd.analyticOrderAt_ne_top_of_isPreconnected propagates the finite order there to every point.

Main results

• TauCeti.analyticOrderNatAt_le_finsum_ball — the order of vanishing at a single point of the open disc is at most the total count.
• TauCeti.finsum_analyticOrderNatAt_ball_eq_zero_of_forall_ne_zero — a zero-free function has count 0.
• TauCeti.finsum_analyticOrderNatAt_ball_eq_zero_iff — conversely, given a point of the closed disc where f does not vanish, a count of 0 means there is no zero in the open disc at all.

theorem TauCeti.analyticOrderNatAt_le_finsum_ball {f : ℂ → ℂ} {c : ℂ} {R : ℝ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall c R)) {z₀ : ℂ} (hz₀ : z₀ ∈ Metric.ball c R) : analyticOrderNatAt f z₀ ≤ ∑ᶠ (z : ℂ) (_ : z ∈ Metric.ball c R), analyticOrderNatAt f z

The order of vanishing at a single point of the open disc is at most the total zero count. Both sides read 0 at a point of infinite order, so the bound is trivially true there too.

The finiteness the sum needs is MeromorphicOn.divisor_ball_support_finite, transported along TauCeti.Contour.divisor_eq_analyticOrderNatAt.

theorem TauCeti.finsum_analyticOrderNatAt_ball_eq_zero_of_forall_ne_zero {f : ℂ → ℂ} {c : ℂ} {R : ℝ} (hf : AnalyticOnNhd ℂ f (Metric.ball c R)) (hne : ∀ z ∈ Metric.ball c R, f z ≠ 0) : ∑ᶠ (z : ℂ) (_ : z ∈ Metric.ball c R), analyticOrderNatAt f z = 0

A function holomorphic and zero-free on the open disc has zero count 0 there.

theorem TauCeti.finsum_analyticOrderNatAt_ball_eq_zero_iff {f : ℂ → ℂ} {c : ℂ} {R : ℝ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall c R)) (hne : ∃ z ∈ Metric.closedBall c R, f z ≠ 0) : ∑ᶠ (z : ℂ) (_ : z ∈ Metric.ball c R), analyticOrderNatAt f z = 0 ↔ ∀ z ∈ Metric.ball c R, f z ≠ 0

The zero count detects zeros. For f holomorphic on closedBall c R and nonvanishing at some point of that closed disc, the count ∑ᶠ z ∈ ball c R, analyticOrderNatAt f z vanishes precisely when f has no zero in the open disc.

The nontrivial direction is that a zero contributes a nonzero order. That fails without a hypothesis of this kind: analyticOrderNatAt sends a point of infinite order to 0, so the identically zero function has count 0 while vanishing everywhere. A single point of nonvanishing rules that out, the closed disc being preconnected.