The Hungerbühler–Wasem generalized residue theorem

The summit of the contour-integration roadmap (HW Thm 3.3): for f holomorphic on U ∖ S and meromorphic at each point of the finite S ⊆ U, and a null-homologous, closed piecewise-C¹ immersion γ in U rooted off the poles, under the regularity conditions (A′) and (B), the set-level Cauchy principal value of f along γ exists and equals 2πi · Σ_{s ∈ S} n_s(γ) · Res_s f — with the generalized (non-integer) winding numbers as weights, valid when singularities lie on the curve. The half-residue case (S = {s}, n_s(γ) = ½) evaluates to πi · Res_s f — the on-cycle acceptance gate, and the value the valence formula uses at i and ρ.

Both statements follow the roadmap signatures. The proof instantiates the canonical polar decomposition, discharges the conditions into the per-pole hypotheses, and assembles the residue sum; a reversed parametrization (b ≤ a) reduces to the oriented case through the orientation lemmas, every ingredient being endpoint-swap invariant. That assembly is kept separate from the null-homology hypothesis, which enters only at the last step to kill the analytic remainder — so the splitting it factors through is available to callers that must add several curves up before any of them bounds.

Main results

• Contour.PolarPartDecomposition.hasCauchyPV_analyticRemainder_add_residue_sum_of_conditions — the null-homology-free splitting of the principal value into the analytic remainder's contour integral and the winding-weighted residue sum, in either parametrization orientation.
• Contour.hungerbuhlerWasem_residueTheorem — HW Thm 3.3.
• Contour.hasCauchyPV_half_residue — the winding-½ on-cycle case.
• Contour.hungerbuhlerWasem_residueTheorem_of_simple_poles, Contour.hasCauchyPV_half_residue_of_simple_pole — the simple-pole forms, with conditions (A′) and (B) discharged automatically; the statements the argument principle and the valence formula consume.

Provenance

Migrated from residueTheorem_crossing_paper_faithful_clean of MultiCrossingCPV.lean (re-exported as hw_3_3_clean_full_mero in HW33Clean.lean) in the AINTLIB LeanModularForms development, restated for a raw curve over [a, b]; the basepoint hypothesis hγa is that statement's hx_notin_S. See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, Thm 3.3.

theorem TauCeti.Contour.PolarPartDecomposition.hasCauchyPV_analyticRemainder_add_residue_sum_of_conditions {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} (decomp : PolarPartDecomposition f S U) (hU : IsOpen U) (h_ord : ∀ (s : ↥S), decomp.order s = meromorphicPolarOrderAt f ↑s) (hSU : ↑S ⊆ U) {γ : ℝ → ℂ} {a b : ℝ} (hγ_imm : IsPwC1ImmersionOn γ a b) (hclosed : γ a = γ b) (hγa : γ a ∉ ↑S) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hmero : ∀ s ∈ S, MeromorphicAt f s) (hA : ConditionAprime γ a b f S) (hB : ConditionB γ a b f) : HasCauchyPV γ a b f ((∫ (t : ℝ) in a..b, deriv γ t • decomp.analyticRemainder (γ t)) + 2 * ↑Real.pi * Complex.I * ∑ s ∈ S, windingNumber γ a b s * residue f s)

The winding-weighted residue sum splits off the generalized principal value. For f holomorphic on U ∖ S and meromorphic at each point of the finite S ⊆ U, and a closed piecewise-C¹ immersion γ in U rooted off the poles, under conditions (A′) and (B) the set-level Cauchy principal value of f along γ is the ordinary contour integral of the analytic remainder of a polar decomposition plus 2πi · Σ_{s ∈ S} n_s(γ) · Res_s f.

No null-homology is asked of γ, so this is the form that survives being summed over the generators of a formal cycle, none of which need bound on its own (TauCeti.Contour.Cycle.hungerbuhlerWasem_residueTheorem). Discharging the analytic remainder by the homology Cauchy theorem recovers HW Thm 3.3 itself.

Both parametrization orientations are covered: the reversed case reduces to a ≤ b on (b, a) through the orientation lemmas, every ingredient being endpoint-swap invariant.

theorem TauCeti.Contour.hungerbuhlerWasem_residueTheorem {f : ℂ → ℂ} {U : Set ℂ} (hU : IsOpen U) (S : Finset ℂ) (γ : ℝ → ℂ) (a b : ℝ) (hγ_imm : IsPwC1ImmersionOn γ a b) (hSU : ↑S ⊆ U) (hclosed : γ a = γ b) (hγa : γ a ∉ ↑S) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hf : DifferentiableOn ℂ f (U \ ↑S)) (hmero : ∀ s ∈ S, MeromorphicAt f s) (hnull : IsNullHomologous γ a b U) (hA : ConditionAprime γ a b f S) (hB : ConditionB γ a b f) : HasCauchyPV γ a b f (2 * ↑Real.pi * Complex.I * ∑ s ∈ S, windingNumber γ a b s * residue f s)

The Hungerbühler–Wasem generalized residue theorem (HW Thm 3.3): for f holomorphic on U ∖ S and meromorphic at each point of the finite S ⊆ U, and a null-homologous closed piecewise-C¹ immersion γ in U rooted off the poles, under conditions (A′) and (B) the set-level Cauchy principal value of f along γ is 2πi · Σ_{s ∈ S} n_s(γ) · Res_s f, with the generalized (non-integer) winding numbers as weights — valid when singularities of f lie on the curve.

theorem TauCeti.Contour.hasCauchyPV_half_residue {f : ℂ → ℂ} {U : Set ℂ} (hU : IsOpen U) (γ : ℝ → ℂ) (a b : ℝ) (s : ℂ) (hγ_imm : IsPwC1ImmersionOn γ a b) (hsU : s ∈ U) (hclosed : γ a = γ b) (hγa : γ a ≠ s) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hf : DifferentiableOn ℂ f (U \ {s})) (hmero : MeromorphicAt f s) (hnull : IsNullHomologous γ a b U) (hA : ConditionAprime γ a b f {s}) (hB : ConditionB γ a b f) (hwind : windingNumber γ a b s = 1 / 2) : HasCauchyPV γ a b f (↑Real.pi * Complex.I * residue f s)

Half-residue: the winding-½ on-cycle case of HW Thm 3.3 — the S = {s} specialisation: when the generalized winding number of the closed, null-homologous immersion about the on-cycle singularity s is ½, the principal value is πi · Res_s f.

The simple-pole form

When every prescribed singularity is at worst a simple pole, conditions (A′) and (B) hold automatically — first-order flatness is every immersion's geometry, and the sector condition only constrains poles of order > 1. This is HW's own base regime (Thm 3.3's unconditional case, "C only contains singularities of f which are poles of order 1"), and the form the argument principle and the valence formula consume: a logarithmic derivative has only simple poles.

theorem TauCeti.Contour.conditionAprime_of_simple_poles {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {U : Set ℂ} {S : Finset ℂ} (hU : IsOpen U) (hγ_imm : IsPwC1ImmersionOn γ a b) (hymin : γ (min a b) ∉ ↑S) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hf : DifferentiableOn ℂ f (U \ ↑S)) (h_simple : ∀ s ∈ S, ↑(-1) ≤ meromorphicOrderAt f s) : ConditionAprime γ a b f S

Condition (A′) is automatic at simple poles. The only pole order the interior clause can meet is 1, discharged by the first-order flatness of the immersion, and the basepoint γ (min a b) is off the singularities.

The curve need not be closed: ConditionAprime constrains the basepoint γ (min a b), so hymin is the whole premise the proof consumes. A closed contour supplies it from γ a = γ b together with γ a ∉ S, which is what hungerbuhlerWasem_residueTheorem_of_simple_poles does at its call site.

This is an instantiation lemma for TauCeti.Contour.ConditionAprime: it exhibits a hypothesis set a caller can actually supply — a piecewise-C¹ immersion whose basepoint lies off S, with f having at worst simple poles — under which the condition holds. Where an interior crossing occurs the flatness clause is met with content rather than by vacuity: the pole order there is forced to 1 and IsPwC1ImmersionOn.flatOfOrder_one supplies the first-order flatness. On a curve with no interior crossing the clause holds because there is nothing to discharge.

theorem TauCeti.Contour.conditionB_of_simple_poles {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {U : Set ℂ} {S : Finset ℂ} (hU : IsOpen U) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hf : DifferentiableOn ℂ f (U \ ↑S)) (h_simple : ∀ s ∈ S, ↑(-1) ≤ meromorphicOrderAt f s) : ConditionB γ a b f

Condition (B) is automatic at simple poles. Its clauses only fire at poles of order > 1, and there are none.

The companion instantiation lemma to conditionAprime_of_simple_poles: together the two discharge both regularity hypotheses of HW Thm 3.3 from the same simple-pole hypothesis, which is what makes hungerbuhlerWasem_residueTheorem_of_simple_poles unconditional.

theorem TauCeti.Contour.hungerbuhlerWasem_residueTheorem_of_simple_poles {f : ℂ → ℂ} {U : Set ℂ} (hU : IsOpen U) (S : Finset ℂ) (γ : ℝ → ℂ) (a b : ℝ) (hγ_imm : IsPwC1ImmersionOn γ a b) (hSU : ↑S ⊆ U) (hclosed : γ a = γ b) (hγa : γ a ∉ ↑S) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hf : DifferentiableOn ℂ f (U \ ↑S)) (hmero : ∀ s ∈ S, MeromorphicAt f s) (hnull : IsNullHomologous γ a b U) (h_simple : ∀ s ∈ S, ↑(-1) ≤ meromorphicOrderAt f s) : HasCauchyPV γ a b f (2 * ↑Real.pi * Complex.I * ∑ s ∈ S, windingNumber γ a b s * residue f s)

The generalized residue theorem for simple poles — HW Thm 3.3's unconditional regime: when every prescribed singularity is at worst a simple pole (meromorphicOrderAt f s ≥ -1), conditions (A′) and (B) hold automatically, and the principal value is the winding-weighted residue sum with no regularity hypotheses beyond the immersion. The form the argument principle and the valence formula consume.

theorem TauCeti.Contour.hasCauchyPV_half_residue_of_simple_pole {f : ℂ → ℂ} {U : Set ℂ} (hU : IsOpen U) (γ : ℝ → ℂ) (a b : ℝ) (s : ℂ) (hγ_imm : IsPwC1ImmersionOn γ a b) (hsU : s ∈ U) (hclosed : γ a = γ b) (hγa : γ a ≠ s) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hf : DifferentiableOn ℂ f (U \ {s})) (hmero : MeromorphicAt f s) (hnull : IsNullHomologous γ a b U) (h_simple : ↑(-1) ≤ meromorphicOrderAt f s) (hwind : windingNumber γ a b s = 1 / 2) : HasCauchyPV γ a b f (↑Real.pi * Complex.I * residue f s)

The half-residue theorem at a simple pole: the winding-½ case with the conditions discharged automatically — an on-cycle simple pole crossed by the immersion contributes πi · Res_s f. The acceptance form for the valence formula's i and ρ.