The residue of the logarithmic derivative is the meromorphic order

For f : ℂ → ℂ meromorphic at z₀ of order n = meromorphicOrderAt f z₀, the residue of the logarithmic derivative there is exactly that order: TauCeti.Contour.residue (logDeriv f) z₀ = n. This is the residue-form of the argument principle, the identity Res_{z₀}(f'/f) = ord_{z₀} f that the roadmap names as the local statement its contour form (TauCeti.Contour.argumentPrinciple) integrates: a zero of order k contributes +k and a pole of order k contributes −k.

The mechanism is the simple-pole splitting of the logarithmic derivative (TauCeti.Contour.logDeriv_eventuallyEq_principalPart): near z₀ there is g analytic and non-vanishing with logDeriv f = n · (· − z₀)⁻¹ + logDeriv g on a punctured neighbourhood. The analytic tail logDeriv g contributes no residue, so only the simple-pole principal part n · (· − z₀)⁻¹ survives, whose residue is n by TauCeti.Contour.residue_const_mul_sub_inv (the elementary simple-pole residues live in TauCeti.Analysis.Contour.Residue.SimplePole).

Main results

• TauCeti.Contour.residue_logDeriv_eq_meromorphicOrderAt — residue (logDeriv f) z₀ = n when meromorphicOrderAt f z₀ = n: the residue of f'/f is the order of f at z₀.

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

Provenance

The simple-pole splitting logDeriv_eventuallyEq_principalPart and the residue API are adapted from the AINTLIB LeanModularForms project (the argument-principle and residue material of ForMathlib/GeneralizedResidueTheory/Residue.lean and .../Residue/GeneralizedTheoremBase.lean, where the residue theorem is applied to logDeriv f), here specialised to Mathlib's meromorphicOrderAt API and 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.residue_logDeriv_eq_meromorphicOrderAt {f : ℂ → ℂ} {z₀ : ℂ} {n : ℤ} (hf : MeromorphicAt f z₀) (hn : meromorphicOrderAt f z₀ = ↑n) : residue (logDeriv f) z₀ = ↑n

The residue of the logarithmic derivative is the meromorphic order. If f is meromorphic at z₀ of order n (meromorphicOrderAt f z₀ = n), then residue (logDeriv f) z₀ = n: the residue of f'/f counts the order of f at z₀ — positive at a zero, negative at a pole. This is the local, residue-form of the argument principle TauCeti.Contour.argumentPrinciple, the identity Res_{z₀}(f'/f) = ord_{z₀} f.