The classical residue theorem for contour cycles #
This file extends the classical residue theorem from one parametrized closed curve to a finite
formal integer cycle C of such curves. For f differentiable on U ∖ S and meromorphic at each
point of the finite set S lying in U, and a cycle C in U that is null-homologous there
and whose trace avoids S,
Cycle.integral f C = 2πi · ∑_{s ∈ S} n_s(C) · Res_s f,
each pole weighted by the generalized winding number of the cycle about it.
The extension is not a formal consequence of the single-curve theorem
(TauCeti.Contour.classicalResidueTheorem_nullHomologous) applied generator by generator: null
homology is imposed on C alone, and its individual generators need not be null-homologous — the
whole point of allowing formal integer combinations is that a cycle can bound while its pieces do
not. What does split over the support is the residue half of the argument. So the proof runs one
rung lower down: a fixed polar-part decomposition f = g + ∑_{s ∈ S} P_s on U is chosen once,
and the null-homology-free identity
∮_γ f = ∮_γ g + 2πi · ∑_{s ∈ S} n_s(γ) · Res_s f
(PolarPartDecomposition.intervalIntegral_deriv_smul_eq_analyticRemainder_add_sum) is summed over
the generators of C with their coefficients. 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. Its S = ∅ case is exactly that theorem.
Cauchy's integral formula for a cycle follows, as usual, by applying the residue theorem to the
Cauchy kernel w ↦ f w / (w − z) ^ (k + 1), whose only singularity in U is at z.
Main results #
TauCeti.Contour.Cycle.integral_eq_analyticRemainder_add_sum— the residue sum splits off the cycle integral for a fixed polar-part decomposition, before any null-homology hypothesis is used.TauCeti.Contour.Cycle.classicalResidueTheorem_nullHomologous— the residue theorem for a null-homologous cycle avoiding the poles.TauCeti.Contour.Cycle.cauchyIntegralFormula_iteratedDeriv_nullHomologous,TauCeti.Contour.Cycle.cauchyIntegralFormula_nullHomologousandTauCeti.Contour.Cycle.cauchyIntegralFormula_deriv_nullHomologous— Cauchy's integral formula for a cycle, for every iterated derivative and forfandf'themselves.
References #
- N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997 (2018), §3.
- S. Lang, Complex Analysis (GTM 103), Ch. VI (the homology form of the residue theorem for cycles).
- L. Ahlfors, Complex Analysis, Ch. 4.
Provenance #
No formal source is vendored: the statements are assembled here from the repository's polar-part
decomposition and its homology Cauchy theorem for cycles, which are themselves migrated from the
AINTLIB LeanModularForms development.
The residue sum splits off a cycle integral. For a fixed polar-part decomposition of f on
U at S, a cycle lying in U whose trace avoids S integrates to the integral of the analytic
remainder plus 2πi times the winding-weighted residue sum.
Nothing is assumed here about f beyond the decomposition, and — crucially for the cycle case —
nothing about null-homology: the identity is summed from its single-curve form
(TauCeti.Contour.PolarPartDecomposition.intervalIntegral_deriv_smul_eq_analyticRemainder_add_sum)
over the generators of the cycle, each of which may wind arbitrarily around the holes of U.
The classical residue theorem for a null-homologous contour cycle. Let U be open, S a
finite set, f differentiable on U ∖ S and meromorphic at each point of S lying in U, and let
C be a contour cycle in U, null-homologous in U, whose trace avoids S. Then
Cycle.integral f C = 2πi · ∑_{s ∈ S} n_s(C) · Res_s f,
each pole weighted by the generalized winding number of C about it.
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 loops around a hole of U, neither
of them null-homologous, is. Points of S outside U are harmless rather than excluded, their
winding number vanishing by null-homology, and S may list regular points of f, whose residues
are 0.
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.classicalResidueTheorem_nullHomologous.
Cauchy's integral formula for a cycle, for the k-th derivative. Let f be holomorphic on
an open U, let C be a contour cycle in U that is null-homologous there, and let z ∈ U lie
off the trace of C. Then for every k,
Cycle.integral (fun w ↦ f w / (w − z) ^ (k + 1)) C = 2πi · n_z(C) · f⁽ᵏ⁾(z) / k !.
Only the residue at z contributes: the residue theorem for a null-homologous cycle applied to the
Cauchy kernel w ↦ f w / (w − z) ^ (k + 1), whose only possible singularity in U is at z.
Cauchy's integral formula for a cycle (roadmap Layer 3). For f holomorphic on an open U,
C a contour cycle in U that is null-homologous there, and z ∈ U off the trace of C,
Cycle.integral (fun w ↦ f w / (w − z)) C = 2πi · n_z(C) · f z,
so that f z · n_z(C) = (2πi)⁻¹ ∮_C f(w)/(w − z) dw: the Cauchy-type integral over the cycle
recovers the value of f at z, counted with the multiplicity with which C winds around it. The
S = ∅ companion of this statement is the homology Cauchy theorem for cycles
(TauCeti.Contour.Cycle.homologyCauchyTheorem).
Cauchy's integral formula for a cycle, first derivative. The k = 1 case of
TauCeti.Contour.Cycle.cauchyIntegralFormula_iteratedDeriv_nullHomologous, stated with
deriv f z:
Cycle.integral (fun w ↦ f w / (w − z) ^ 2) C = 2πi · n_z(C) · f' z.