Generalized Residue Theorem -- Public API

Clean top-level names for the generalized residue theorem and its corollaries. All proofs delegate to the machinery in HomologicalCauchy.lean and Residue/FlatnessTransfer.lean; this file contains no new proof work.

Main results

• generalizedResidueTheorem -- the most general version: null-homologous curve, higher-order poles, conditions (A')+(B).
• generalizedResidueTheorem_simplePoles -- corollary for simple poles in null-homologous setting (conditions A+B drop out; uses HasSimplePoleAt).

References

• Hungerbuhler-Wasem, The generalized residue theorem, arXiv:1808.00997v2, Theorem 3.3.

Master theorem (null-homologous, higher-order poles, conditions A'+B)

theorem generalizedResidueTheorem (U : Set ℂ) (hU : IsOpen U) (S : Set ℂ) (hS_in_U : ∀ s ∈ S, s ∈ U) (hS_discrete : ∀ s ∈ S, ∃ ε > 0, ∀ s' ∈ S, s' ≠ s → ε ≤ ‖s' - s‖) (hS_closed : IsClosed S) (S0 : Finset ℂ) (hS0_subset : ∀ s ∈ S0, s ∈ S) (f : ℂ → ℂ) (hf : DifferentiableOn ℂ f (U \ ↑S0)) (γ : PiecewiseC1Immersion) (h_null : IsNullHomologous γ U) (hS_on_curve : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ∈ S → γ.toFun t ∈ S0) (hMero : ∀ s ∈ S0, MeromorphicAt f s) (hCondA : SatisfiesConditionA' γ S0 fun (s : ℂ) => poleOrderAt f s) (hCondB : SatisfiesConditionB γ f S0) (hγ_meas : Measurable γ.toFun) (h_no_endpt_cross : ∀ s ∈ S0, γ.toFun γ.a ≠ s ∧ γ.toFun γ.b ≠ s) (h_unique_cross : ∀ s ∈ S0, ∀ t₁ ∈ Set.Icc γ.a γ.b, ∀ t₂ ∈ Set.Icc γ.a γ.b, γ.toFun t₁ = s → γ.toFun t₂ = s → t₁ = t₂) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in γ.a..γ.b, cauchyPrincipalValueIntegrandOn S0 f γ.toFun ε t) (nhdsWithin 0 (Set.Ioi 0)) (nhds (2 * ↑Real.pi * Complex.I * ∑ s ∈ S0, generalizedWindingNumber' γ.toFun γ.a γ.b s * residueAt f s))

Generalized Residue Theorem (Hungerbuhler-Wasem, Theorem 3.3).

For a meromorphic function f with finitely many poles S0 on a null-homologous piecewise C^1 immersion gamma in an open set U, the Cauchy principal value integral converges to 2 pi i * sum_{s in S0} n(gamma, s) * Res(f, s), provided conditions (A') (flatness) and (B) (angle/Laurent compatibility) hold at every crossing point.

This is the most general form. See generalizedResidueTheorem_simplePoles for the simple-pole case where conditions A'+B are not needed.

Simple-pole corollary

theorem generalizedResidueTheorem_simplePoles (U : Set ℂ) (hU : IsOpen U) (S : Set ℂ) (hS_in_U : ∀ s ∈ S, s ∈ U) (hS_discrete : ∀ s ∈ S, ∃ ε > 0, ∀ s' ∈ S, s' ≠ s → ε ≤ ‖s' - s‖) (hS_closed : IsClosed S) (S0 : Finset ℂ) (hS0_subset : ∀ s ∈ S0, s ∈ S) (f : ℂ → ℂ) (hf : DifferentiableOn ℂ f (U \ ↑S0)) (γ : PiecewiseC1Immersion) (h_null : IsNullHomologous γ U) (hS_on_curve : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ∈ S → γ.toFun t ∈ S0) (hSimplePoles : ∀ s ∈ S0, HasSimplePoleAt f s) (hf_ext : ∀ s ∈ S0, ContinuousAt (fun (z : ℂ) => f z - residueSimplePole f s / (z - s)) s) (_hγ_meas : Measurable γ.toFun) (h_no_endpt_cross : ∀ s ∈ S0, γ.toFun γ.a ≠ s ∧ γ.toFun γ.b ≠ s) (h_unique_cross : ∀ s ∈ S0, ∀ t₁ ∈ Set.Icc γ.a γ.b, ∀ t₂ ∈ Set.Icc γ.a γ.b, γ.toFun t₁ = s → γ.toFun t₂ = s → t₁ = t₂) : cauchyPrincipalValueOn S0 f γ.toFun γ.a γ.b = 2 * ↑Real.pi * Complex.I * ∑ s ∈ S0, generalizedWindingNumber' γ.toFun γ.a γ.b s * residueAt f s

Generalized Residue Theorem for simple poles (null-homologous).

When every singularity in S0 is a simple pole, conditions (A') and (B) are not needed: condition (A') is automatic because every piecewise C^1 immersion is flat of order 1 (isFlatOfOrder_one), and the Laurent compatibility in condition (B) is vacuously satisfied (no higher-order terms). The conclusion is an equality (CPV exists), not just Tendsto, and uses residueAt in place of residueSimplePole.

Self-contained proof. Decomposes f = g + Σ res/(z-s) where g is holomorphic on U. Dixon gives ∮ g dz = 0, so CPV(g) → 0. The convex theorem on (univ, convex_univ) gives CPV(f_sing) = 2πi · Σ n · Res. Adding the two yields CPV(f) = CPV(f_sing).

Hypotheses compared to generalizedResidueTheorem:

• Replaces hCondA, hCondB with hSimplePoles (simple pole at each s) and hf_ext (continuity of the regular part f(z) - Res/(z-s)).
• Requires DifferentiableOn of f on U \ S0.