The argument principle against the divisor

TauCeti.Contour.argumentPrinciple asks its caller for the data of the counting problem: a finite set S collecting the nonzero-order points, an order function ord, and proofs that the two agree and that S is exhaustive. Mathlib's MeromorphicOn.divisor already packages exactly that data — MeromorphicOn.divisor_apply evaluates it to (meromorphicOrderAt f z).untop₀, and MeromorphicOn.divisor_ball_support_finite supplies the finiteness from the same MeromorphicOn f (closedBall c R) hypothesis the argument principle already assumes. This file restates the argument principle against that API, so callers that already speak divisor need not rebuild the finset and the order function by hand.

The only hypothesis this adds is hsphere: the bounding circle carries no zeros or poles. It does double duty.

• It confines the nonzero-order points to the open disc, so a divisor taken over ball c R still accounts for every such point of closedBall c R.
• It rules out order ⊤. This matters because (⊤ : WithTop ℤ).untop₀ = 0, so at a point where f vanishes identically the divisor reads 0 while the order does not, and the exhaustiveness obligation of argumentPrinciple would fail exactly there. No separate hypothesis is needed: closedBall c R is convex, hence preconnected, and the sphere is nonempty as 0 < R, so MeromorphicOn.meromorphicOrderAt_ne_top_of_isPreconnected propagates the finite order at a boundary point to the whole disc.

Main results

• TauCeti.Contour.argumentPrinciple_divisor — ∮_{C(c,R)} logDeriv f = 2πi · ∑ᶠ z, divisor f (ball c R) z, the argument principle with the counting data taken from MeromorphicOn.divisor. The conclusion uses the canonical finitely supported sum ∑ᶠ, which is well defined because the divisor vanishes off ball c R; the finiteness witness MeromorphicOn.divisor_ball_support_finite stays inside the proof rather than appearing in the statement.

References

• N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997.

theorem TauCeti.Contour.divisor_eq_analyticOrderNatAt {f : ℂ → ℂ} {U : Set ℂ} {z : ℂ} (hm : MeromorphicOn f U) (hf : AnalyticAt ℂ f z) (hz : z ∈ U) : (MeromorphicOn.divisor f U) z = ↑(analyticOrderNatAt f z)

Where a meromorphic function is analytic, its divisor records the order of vanishing. The identity also holds at a point of infinite order, where both sides read 0.

This is the bridge between MeromorphicOn.divisor — whose support is finite on a ball by MeromorphicOn.divisor_ball_support_finite — and the analyticOrderNatAt vocabulary that zero counts are stated in, so zero-counting arguments can reuse it instead of rebuilding the correspondence. Note the finiteness is of the divisor's support, equivalently of the zeros of finite order: a point where f vanishes identically has divisor value 0 and is absent from it.

theorem TauCeti.Contour.argumentPrinciple_divisor {f : ℂ → ℂ} {c : ℂ} {R : ℝ} (hR : 0 < R) (hf : MeromorphicOn f (Metric.closedBall c R)) (hsphere : ∀ z ∈ Metric.sphere c R, meromorphicOrderAt f z = 0) : circleIntegral (logDeriv f) c R = 2 * ↑Real.pi * Complex.I * ∑ᶠ (z : ℂ), ↑((MeromorphicOn.divisor f (Metric.ball c R)) z)

The argument principle, against the divisor. For f meromorphic on the closed disc C(c, R) with no zero or pole on the bounding circle, the contour integral of the logarithmic derivative is 2πi times the sum of MeromorphicOn.divisor over the open disc.

This is TauCeti.Contour.argumentPrinciple with the finite set and the order function supplied by Mathlib's divisor API rather than by the caller.