The argument principle

For f : ℂ → ℂ meromorphic on a closed disc C(c, R) whose nonzero-order points are contained in a finite set S inside the open disc, on which ord z = meromorphicOrderAt f z, the contour integral of the logarithmic derivative counts the zeros and poles with multiplicity: ∮_{C(c,R)} f'/f = 2πi · ∑_{z ∈ S} ord z.

The order ord z = meromorphicOrderAt f z is positive at a zero and negative at a pole, so the integral is 2πi times the number of zeros minus poles inside the circle. The one-point special case — the centre c is the only point that may have nonzero order — is argumentPrinciple_local.

This is the argument-principle contour identity the valence formula evaluates over the interior orbits: the residue of f'/f at a point is its meromorphic order there. Mathlib has logDeriv and meromorphicOrderAt but not this identity.

Only the finite set S is required to lie in the open disc; away from S every point of the closed disc has order 0, hence is at worst a removable singularity of f. No pointwise regularity of the raw function f is hypothesised — f may take isolated "wrong values" where logDeriv f is meaningless — since the results are stated up to the meromorphic normal form of f.

Main results

• TauCeti.Contour.argumentPrinciple — ∮_{C(c,R)} logDeriv f = 2πi · ∑_{z ∈ S} ord z when all nonzero-order points are contained in a finite set S inside the open disc, with ord agreeing with meromorphicOrderAt f on S.
• TauCeti.Contour.neg_one_le_meromorphicOrderAt_logDeriv — a logarithmic derivative has at worst a simple pole, whatever the order of f.
• TauCeti.Contour.argumentPrinciple_local — the special case S = {c}: ∮_{C(c,R)} logDeriv f = 2πi · n when the centre c, of order n, is the only point of the closed disc that may have nonzero meromorphic order.

These are Layer 2 targets of the contour-integration roadmap, feeding the argument principle and, ultimately, the valence formula.

Provenance

Adapted from the AINTLIB LeanModularForms project (the argument-principle specialisation of ForMathlib/GeneralizedResidueTheory/Residue.lean and .../Residue/GeneralizedTheoremBase.lean, where the residue theorem is applied to logDeriv f), specialised to a circle and to the raw-function design of the contour-integration roadmap.

References

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

theorem TauCeti.Contour.logDeriv_eventuallyEq_principalPart {F : ℂ → ℂ} {s : ℂ} {n : ℤ} (hF : MeromorphicAt F s) (hn : meromorphicOrderAt F s = ↑n) : ∃ (g : ℂ → ℂ), AnalyticAt ℂ g s ∧ g s ≠ 0 ∧ logDeriv F =ᶠ[nhdsWithin s {s}ᶜ] fun (z : ℂ) => ↑n * (z - s)⁻¹ + logDeriv g z

Simple-pole splitting of the logarithmic derivative. Near a point s where F is meromorphic of order n, the logarithmic derivative equals its simple-pole principal part n · (· - s)⁻¹ plus an analytic term: there is g analytic and non-vanishing at s (the local factor of F = (· - s) ^ n • g) with logDeriv F = n · (· - s)⁻¹ + logDeriv g on a punctured neighbourhood of s. Exposed for the residue-form of the argument principle (TauCeti.Contour.residue_logDeriv_eq_meromorphicOrderAt).

theorem TauCeti.Contour.neg_one_le_meromorphicOrderAt_logDeriv {f : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) : ↑(-1) ≤ meromorphicOrderAt (logDeriv f) z₀

A logarithmic derivative has at worst a simple pole. If f is meromorphic at z₀, of whatever order, then meromorphicOrderAt (logDeriv f) z₀ ≥ -1.

Differentiating cannot make the pole worse than simple however deep the zero or pole of f is: a zero of order n contributes n/(z - z₀), whose order is -1 irrespective of n. Sharply, the order is -1 exactly when ord_{z₀} f ≠ 0, is ≥ 0 when ord_{z₀} f = 0, and is ⊤ when f vanishes identically near z₀.

Meromorphy is essential rather than bookkeeping: at an essential singularity the bound fails, the logarithmic derivative of z ↦ exp (-z⁻¹) being z ↦ (z ^ 2)⁻¹, of order -2 at 0.

This is what puts the argument principle into the unconditional simple-pole regime of the Hungerbühler–Wasem residue theorem, where a contour may run through the zeros (TauCeti.Contour.hasCauchyPV_logDeriv_nullHomologous).

theorem TauCeti.Contour.argumentPrinciple {f : ℂ → ℂ} {c : ℂ} {R : ℝ} (hR : 0 < R) (S : Finset ℂ) (ord : ℂ → ℤ) (hf : MeromorphicOn f (Metric.closedBall c R)) (hS : ↑S ⊆ Metric.ball c R) (hsupp : ∀ z ∈ Metric.closedBall c R, meromorphicOrderAt f z ≠ 0 → z ∈ S) (hord : ∀ z ∈ S, meromorphicOrderAt f z = ↑(ord z)) : circleIntegral (logDeriv f) c R = 2 * ↑Real.pi * Complex.I * ∑ z ∈ S, ↑(ord z)

The argument principle. If f is meromorphic on the closed disc C(c, R) (R > 0) with all its nonzero-order points contained in a finite set S inside the open disc, with orders ord, then the contour integral of the logarithmic derivative counts the zeros minus the poles with multiplicity: ∮_{C(c,R)} f'/f = 2πi · ∑_{z ∈ S} ord z.

theorem TauCeti.Contour.argumentPrinciple_local {f : ℂ → ℂ} {c : ℂ} {R : ℝ} {n : ℤ} (hR : 0 < R) (hf : MeromorphicOn f (Metric.closedBall c R)) (honly : ∀ z ∈ Metric.closedBall c R, meromorphicOrderAt f z ≠ 0 → z = c) (hn : meromorphicOrderAt f c = ↑n) : circleIntegral (logDeriv f) c R = 2 * ↑Real.pi * Complex.I * ↑n

Local argument principle. If f is meromorphic on the closed disc C(c, R) (R > 0) and the centre c is the only point of the disc that may have nonzero meromorphic order — every other point is at worst a removable singularity — then the contour integral of the logarithmic derivative recovers the order n = meromorphicOrderAt f c at the centre: ∮_{C(c,R)} f'/f = 2πi · n. Thus the integral counts the zero (n > 0) or pole (n < 0) at the centre with multiplicity, and vanishes when c too has order 0. This is the S = {c} case of argumentPrinciple.