Documentation

TauCeti.Analysis.Contour.Residue.Cycle

The classical residue theorem for an arbitrary null-homologous cycle #

For f differentiable on U ∖ S and meromorphic at each point of the finite set S lying in U, and a closed, null-homologous piecewise-C¹ curve γ in U that avoids S,

∫ t in a..b, γ' t • f (γ t) = 2πi · ∑_{s ∈ S} n_s(γ) · Res_s f,

where n_s(γ) is the generalized winding number of γ about s. This is the general arbitrary-cycle form of the classical residue theorem, and it generalizes the circle theorem (Contour.classicalResidueTheorem_circle): the contour is an arbitrary piecewise-C¹ loop rather than a round circle, and each pole is weighted by its winding number rather than by 1. Null-homology is not decoration — on a general holomorphy domain Ω, a loop that merely avoids the poles need not integrate to the residue sum (a loop around a hole of Ω sees the function's behaviour there), so n_w(γ) = 0 for every w ∉ Ω is exactly the hypothesis that rules this out. Its S = ∅ case is the homology Cauchy theorem, which is why the roadmap defers this statement past Layer 2.

The proof is the classical three-line argument, over the pieces the repository already has. The polar-part decomposition (Contour.PolarPartDecomposition.ofMeromorphic) writes f = g + ∑_{s ∈ S} P_s on U ∖ S, with g differentiable on all of U and P_s the finite Laurent tail at s. The remainder g integrates to zero by the homology Cauchy theorem (Contour.PolarPartDecomposition.intervalIntegral_deriv_smul_analyticRemainder_eq_zero). In each Laurent tail the simple-pole coefficient integrates to 2πi · n_s(γ) · Res_s f, by the very definition of the winding number (the principal value collapses to an ordinary integral because γ misses s), while every coefficient of order ≥ 2 integrates to zero around the closed curve, having the primitive −(k−1)⁻¹(z − s)^{−(k−1)} (Contour.integral_pow_inv_mul_deriv_eq_zero_of_closed).

Unlike the Hungerbühler–Wasem generalized residue theorem (Contour.hungerbuhlerWasem_residueTheorem), whose singularities may lie on the curve, nothing here needs an immersion, a principal value, or the conditions (A′)/(B): with the poles off the contour every integral in sight is an ordinary interval integral. Conversely this statement is not a specialization of the HW theorem, which asks for the strictly stronger Contour.IsPwC1ImmersionOn regularity, so a piecewise-C¹ loop with a zero-speed seam is covered here and not there.

Main results #

This is the "general arbitrary-cycle case" of the contour-integration roadmap, which that roadmap defers to Layer 3+.

References #

Provenance #

No formal source is vendored: the statement is assembled here from the repository's polar-part decomposition, homology Cauchy theorem, and antiderivative lemma for higher-order Laurent terms, which are themselves migrated from the AINTLIB LeanModularForms development.

source
theorem TauCeti.Contour.PolarPartDecomposition.intervalIntegral_deriv_smul_polarPart {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} (decomp : PolarPartDecomposition f S U) (s : ↥S) {γ : ℝ → ℂ} {a b : ℝ} (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) (h_ne : ∀ t ∈ Set.uIcc a b, γ t ≠ ↑s) :
∫ (t : ℝ) in a..b, deriv γ t • decomp.polarPart s (γ t) = 2 * ↑Real.pi * Complex.I * windingNumber γ a b ↑s * residue f ↑s

The contour integral of a polar part is the winding-weighted residue. Around a closed piecewise-C¹ curve missing the pole s, the finite Laurent tail of f at s integrates to 2πi · n_s(γ) · Res_s f: the simple-pole coefficient contributes the index integral, which is 2πi times the generalized winding number since the principal value collapses to an ordinary integral off the curve, and every higher-order coefficient contributes zero (Contour.integral_pow_inv_mul_deriv_eq_zero_of_closed).

source
theorem TauCeti.Contour.PolarPartDecomposition.intervalIntegral_deriv_smul_eq_analyticRemainder_add_sum {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} (decomp : PolarPartDecomposition f S U) {γ : ℝ → ℂ} {a b : ℝ} (hγ : IsPiecewiseC1On γ a b) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hclosed : γ a = γ b) (hoff : ∀ t ∈ Set.uIcc a b, γ t ∉ ↑S) :
∫ (t : ℝ) in a..b, deriv γ t • f (γ t) = (∫ (t : ℝ) in a..b, deriv γ t • decomp.analyticRemainder (γ t)) + 2 * ↑Real.pi * Complex.I * ∑ s ∈ S, windingNumber γ a b s * residue f s

Splitting the contour integral off the residue sum. Once f is presented on U as an analytic remainder plus finite Laurent tails at the points of S, a closed piecewise-C¹ curve in U avoiding S integrates to the remainder's integral plus the winding-weighted residue sum: the tail at s contributes 2πi · n_s(γ) · Res_s f by intervalIntegral_deriv_smul_polarPart.

No null-homology is assumed here, so the remainder's integral is left standing; discharging it is what intervalIntegral_deriv_smul_eq_sum_windingNumber_mul_residue does for a null-homologous curve. Keeping the two steps apart lets a cycle whose generators need not be null-homologous — only the cycle as a whole — sum this identity over its support (TauCeti.Contour.Cycle.integral_eq_analyticRemainder_add_sum).

Nothing is assumed about f beyond the decomposition itself: no differentiability or meromorphy hypothesis appears, a decomposition already carrying everything the argument uses. When decomp is obtained from ofMeromorphic, those hypotheses were consumed there.

source
theorem TauCeti.Contour.PolarPartDecomposition.intervalIntegral_deriv_smul_eq_sum_windingNumber_mul_residue {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} (decomp : PolarPartDecomposition f S U) (hU : IsOpen U) {γ : ℝ → ℂ} {a b : ℝ} (hγ : IsPiecewiseC1On γ a b) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hclosed : γ a = γ b) (hoff : ∀ t ∈ Set.uIcc a b, γ t ∉ ↑S) (hnull : IsNullHomologous γ a b U) :
∫ (t : ℝ) in a..b, deriv γ t • f (γ t) = 2 * ↑Real.pi * Complex.I * ∑ s ∈ S, windingNumber γ a b s * residue f s

The residue theorem for a fixed polar-part decomposition. Once f is presented on U as an analytic remainder plus finite Laurent tails at the points of S, a closed null-homologous piecewise-C¹ curve in U avoiding S integrates to the winding-weighted residue sum. This is the sum of the two preceding facts: the remainder contributes nothing (intervalIntegral_deriv_smul_analyticRemainder_eq_zero) and the tails contribute the residue sum (intervalIntegral_deriv_smul_eq_analyticRemainder_add_sum).

source
theorem TauCeti.Contour.classicalResidueTheorem_nullHomologous {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f (U \ ↑S)) (hmero : ∀ s ∈ S, s ∈ U → MeromorphicAt f s) {γ : ℝ → ℂ} {a b : ℝ} (hγ : IsPiecewiseC1On γ a b) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hclosed : γ a = γ b) (hoff : ∀ t ∈ Set.uIcc a b, γ t ∉ ↑S) (hnull : IsNullHomologous γ a b U) :
∫ (t : ℝ) in a..b, deriv γ t • f (γ t) = 2 * ↑Real.pi * Complex.I * ∑ s ∈ S, windingNumber γ a b s * residue f s

The classical residue theorem for an arbitrary null-homologous 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 γ be a closed piecewise-C¹ curve in U, null-homologous in U, that avoids S. Then

∫ t in a..b, γ' t • f (γ t) = 2πi · ∑_{s ∈ S} n_s(γ) · Res_s f,

each pole weighted by the generalized winding number of γ about it.

Points of S outside U are harmless rather than excluded: null-homology forces their winding number, hence their contribution, to vanish, so nothing at all is asked of f there — meromorphicity is required only at the points of S that lie in U. Likewise S may list regular points of f, whose residues are 0.

Its S = ∅ case is the homology Cauchy theorem (Contour.homologyCauchyTheorem), so this is genuinely a Layer 3 statement; the round-circle case with the poles inside is Contour.classicalResidueTheorem_circle, and the version admitting poles on the curve is the Hungerbühler–Wasem theorem Contour.hungerbuhlerWasem_residueTheorem.