The Hungerbühler–Wasem generalized residue theorem for contour cycles #
This file lifts HW Thm 3.3 from one parametrized closed curve to a finite formal integer cycle
C of them. For f holomorphic on U ∖ S and meromorphic at each point of the finite S ⊆ U,
and a cycle C in U that is null-homologous there, whose curves are piecewise-C¹
immersions rooted off S and satisfy the regularity conditions (A′) and (B),
PV ∮_C f = 2πi · ∑_{s ∈ S} n_s(C) · Res_s f,
each singularity weighted by the generalized, non-integer winding number of the cycle about
it — so the singularities may lie on C. This removes the first of the narrowings the
roadmap records for the pinned single-curve form
(TauCeti.Contour.hungerbuhlerWasem_residueTheorem), which the paper states for a cycle.
Just as for the classical residue theorem for cycles
(TauCeti.Contour.Cycle.classicalResidueTheorem_nullHomologous), this is not the single-curve
theorem applied generator by generator. Null homology is asked of C alone: its generators may
each wind around the holes of U, and the point of allowing formal integer combinations is
precisely that a cycle can bound while its pieces do not. So the proof runs one rung lower down.
A polar-part decomposition f = g + ∑_{s ∈ S} P_s on U is fixed once, and the
null-homology-free splitting
PV ∮_γ f = ∮_γ g + 2πi · ∑_{s ∈ S} n_s(γ) · Res_s f
(PolarPartDecomposition.hasCauchyPV_analyticRemainder_add_residue_sum_of_conditions)
is summed over the generators with their coefficients — the principal value being additive over
a cycle by construction (TauCeti.Contour.Cycle.cauchyPV). Only then is the analytic remainder
g discharged, by the homology Cauchy theorem for cycles
(TauCeti.Contour.Cycle.homologyCauchyTheorem), which does see the cancellations between
generators.
The remaining narrowings of the single-curve form are inherited unchanged: S is finite, f is
MeromorphicAt at each of its points, and each generator is rooted off S.
Main results #
TauCeti.Contour.Cycle.hasCauchyPV_analyticRemainder_add_residue_sum— the residue sum splits off the cycle's principal value, before any null-homology hypothesis is used.TauCeti.Contour.Cycle.hungerbuhlerWasem_residueTheorem— HW Thm 3.3 for a null-homologous cycle.TauCeti.Contour.Cycle.hungerbuhlerWasem_residueTheorem_of_simple_poles— the unconditional regime, conditions (A′) and (B) being automatic at worst-simple poles.
Provenance #
No formal source is vendored: the statements are assembled here from this repository's
single-curve Hungerbühler–Wasem theory and its homology Cauchy theorem for cycles, which are
themselves migrated from the AINTLIB LeanModularForms development.
References #
- N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997 (2018), Thm 3.3 — there stated for a cycle.
The residue sum splits off a cycle's principal value. For a fixed polar-part
decomposition of f on U at S, and a cycle in U whose curves are piecewise-C¹
immersions rooted off S and satisfying conditions (A′) and (B), the Cauchy principal value of
f along the cycle exists and is the ordinary cycle integral of the analytic remainder plus
2πi times the winding-weighted residue sum.
Nothing is assumed about null-homology, of the cycle or of its generators: the identity is
summed from its single-curve form
(PolarPartDecomposition.hasCauchyPV_analyticRemainder_add_residue_sum_of_conditions)
over the generators of the cycle, each of which may wind arbitrarily around the holes of U.
The Hungerbühler–Wasem generalized residue theorem for a contour cycle (HW Thm 3.3).
Let U be open, S ⊆ U finite, f holomorphic on U ∖ S and meromorphic at each point of
S, and let C be a contour cycle in U, null-homologous in U, whose curves are
piecewise-C¹ immersions rooted off S and satisfy conditions (A′) and (B). Then the Cauchy
principal value of f along C exists and
PV ∮_C f = 2πi · ∑_{s ∈ S} n_s(C) · Res_s f,
each singularity weighted by the generalized winding number of C about it. The
singularities are allowed to lie on C, where those weights are in general not integers and
the contour integral only exists as a principal value.
Null-homology is asked of the cycle only, never of its generators, so the theorem covers the
combinations that make cycles worth having: a difference of two homologous loops around a hole of
U, neither of them null-homologous, is null-homologous. Its S = ∅ case is the homology Cauchy
theorem for cycles
(TauCeti.Contour.Cycle.homologyCauchyTheorem), and its one-generator case is the single-curve
theorem TauCeti.Contour.hungerbuhlerWasem_residueTheorem. Where the trace of C avoids S
the principal value is an ordinary integral and the statement is the classical residue theorem
for cycles (TauCeti.Contour.Cycle.classicalResidueTheorem_nullHomologous), which needs neither
immersions nor the conditions.
The generalized residue theorem for a contour cycle with simple poles — HW Thm 3.3's
unconditional regime for cycles. When every prescribed singularity is at worst a simple pole,
conditions (A′) and (B) hold automatically along each curve of the cycle
(TauCeti.Contour.conditionAprime_of_simple_poles,
TauCeti.Contour.conditionB_of_simple_poles), leaving no regularity hypotheses beyond the
immersions. This is the form the argument principle consumes, a logarithmic derivative having
only simple poles.