The classical residue theorem on a circle

For f meromorphic on a closed disc C(c, R) (R > 0) whose poles are contained in a finite set S inside the open disc, the contour integral of f around the boundary circle is 2πi times the sum of the residues over S: ∮_{C(c,R)} f = 2πi · ∑_{s ∈ S} residue f s.

The hypothesis on S asks only that every pole — every point of negative meromorphic order — lie in S. S may list further points (zeros, or removable/regular points), whose residues are 0 and so do not affect the sum. No pointwise regularity of the raw function f is required — f may take isolated "wrong values" where it disagrees with its meromorphic normal form — since both sides are stated up to that normal form.

Main results

• TauCeti.Contour.classicalResidueTheorem_circle_of_meromorphicOrderAt_neg — the sharp support form: only the poles (points of negative meromorphic order) need lie in S.
• TauCeti.Contour.classicalResidueTheorem_circle — the form asking every point of nonzero meromorphic order to lie in S; a direct corollary since residues at non-poles vanish.

This is the special case of the Hungerbühler–Wasem generalized residue theorem (HW Thm 3.3) for a round circle.

Provenance

Adapted from the AINTLIB LeanModularForms project (the residue theorem of ForMathlib/GeneralizedResidueTheory/Residue/GeneralizedTheoremBase.lean), specialised to a circle and to raw functions, which are compared through their meromorphic normal form.

References

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

theorem TauCeti.Contour.classicalResidueTheorem_circle_of_meromorphicOrderAt_neg {f : ℂ → ℂ} {c : ℂ} {R : ℝ} (hR : 0 < R) (S : Finset ℂ) (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) : circleIntegral f c R = 2 * ↑Real.pi * Complex.I * ∑ s ∈ S, residue f s

The classical residue theorem on a circle (sharp support form). If f is meromorphic on the closed disc C(c, R) (R > 0) and every pole lies in a finite set S inside the open disc, then the contour integral of f around the boundary circle is 2πi times the sum of the residues over S: ∮_{C(c,R)} f = 2πi · ∑_{s ∈ S} residue f s. S need only contain the poles (the points of negative meromorphic order); residues at points of nonnegative order vanish, so listing extra points leaves the sum unchanged.

theorem TauCeti.Contour.classicalResidueTheorem_circle {f : ℂ → ℂ} {c : ℂ} {R : ℝ} (hR : 0 < R) (S : Finset ℂ) (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) : circleIntegral f c R = 2 * ↑Real.pi * Complex.I * ∑ s ∈ S, residue f s

The classical residue theorem on a circle. If f is meromorphic on the closed disc C(c, R) (R > 0) and every point of nonzero meromorphic order lies in a finite set S inside the open disc, then ∮_{C(c,R)} f = 2πi · ∑_{s ∈ S} residue f s. Since residues at non-poles vanish, classicalResidueTheorem_circle_of_meromorphicOrderAt_neg proves the same conclusion asking only the poles (points of negative order) to lie in S.