Cauchy–Goursat for a pole-free meromorphic function

If A is meromorphic on a closed disc C(c, R) (R ≥ 0) and has non-negative meromorphic order at every point of the disc, then the contour integral of A around the boundary circle vanishes: ∮_{C(c,R)} A = 0.

This is the pole-free base case shared by the argument principle and the classical residue theorem: integrating a meromorphic function with no poles inside the disc gives 0. No pointwise regularity of the raw function A is required — the statement is up to the meromorphic normal form of A, which is genuinely analytic throughout the disc.

Main results

• TauCeti.Contour.circleIntegral_eq_zero_of_meromorphicOrderAt_nonneg — the vanishing of the circle integral of a pole-free meromorphic function.

Provenance

Adapted from the AINTLIB LeanModularForms project, specialised to a circle and to the raw-function design of the contour-integration roadmap.

theorem TauCeti.Contour.circleIntegral_eq_zero_of_meromorphicOrderAt_nonneg {A : ℂ → ℂ} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (hA : MeromorphicOn A (Metric.closedBall c R)) (hord : ∀ z ∈ Metric.closedBall c R, 0 ≤ meromorphicOrderAt A z) : circleIntegral A c R = 0

Cauchy–Goursat for a pole-free meromorphic function. If A is meromorphic on the closed disc C(c, R) (R ≥ 0) and has non-negative meromorphic order at every point of the disc, then ∮_{C(c,R)} A = 0.