Generalized Residue Theorem -- Base Infrastructure

Multi-point PV existence, helper lemmas, and the core generalized residue theorem for piecewise C1 immersions passing through poles. This file provides the infrastructure used by both the convex and null-homologous versions.

Main Results

• cauchyPrincipalValueOn_singular_sum -- multi-point PV exists when each singular term has PV
• generalizedResidueTheorem' -- CPV equals 2 pi i . Sigma winding . residue (convex domain, with explicit PV hypothesis)
• residueAt -- residue via contour integral
• generalizedResidueTheorem_higher_order_tendsto -- higher-order Tendsto formulation (no convexity needed)
• Helper lemmas: hasSimplePoleAt_sum_div_sub, differentiableOn_sum_div_sub, residueSimplePole_sum_div_sub, continuousAt_sum_remainder

The convex-domain theorems generalizedResidueTheorem, generalizedResidueTheorem_higher_order, and generalizedResidueTheorem_higher_order_simple are in GeneralizedTheorem.lean, where they are proved as corollaries of the null-homologous versions.

theorem cauchyPrincipalValueOn_singular_sum (S0 : Finset ℂ) (f : ℂ → ℂ) (γ : PiecewiseC1Immersion) (_hSimplePoles : ∀ s ∈ S0, HasSimplePoleAt f s) (hPV_each : ∀ s ∈ S0, CauchyPrincipalValueExists' (fun (z : ℂ) => residueSimplePole f s / (z - s)) γ.toFun γ.a γ.b s) (hg_reg_cont : ContinuousOn (fun (z : ℂ) => f z - ∑ s ∈ S0, residueSimplePole f s / (z - s)) (γ.toFun '' Set.Icc γ.a γ.b)) : CauchyPrincipalValueExistsOn S0 f γ.toFun γ.a γ.b

Multi-point PV exists when each singular term has PV.

theorem generalizedResidueTheorem' (U : Set ℂ) (hU : IsOpen U) (hU_convex : Convex ℝ 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γ_closed : γ.IsClosed) (hγ_in_U : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ∈ 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) (hPV_singular : ∀ s ∈ S0, CauchyPrincipalValueExists' (fun (z : ℂ) => residueSimplePole f s / (z - s)) γ.toFun γ.a γ.b s) : CauchyPrincipalValueExistsOn S0 f γ.toFun γ.a γ.b ∧ cauchyPrincipalValueOn S0 f γ.toFun γ.a γ.b = 2 * ↑Real.pi * Complex.I * ∑ s ∈ S0, generalizedWindingNumber' γ.toFun γ.a γ.b s * residueSimplePole f s

Generalized residue theorem: CPV equals 2πi · Σ winding · residue even when γ crosses poles.

theorem CauchyPrincipalValueExists'.const_mul {f : ℂ → ℂ} {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (c : ℂ) (h : CauchyPrincipalValueExists' f γ a b z₀) : CauchyPrincipalValueExists' (fun (z : ℂ) => c * f z) γ a b z₀

If PV of f exists, then PV of c * f exists (scaling by constant).

General residue and the higher-order theorem

noncomputable def residueAt (f : ℂ → ℂ) (z₀ : ℂ) : ℂ

Residue of f at z₀ via contour integral: Res(f, z₀) = lim_{r→0⁺} (2πi)⁻¹ ∮_{|z-z₀|=r} f(z) dz.

This is well-defined for meromorphic functions and agrees with residueSimplePole when f has a simple pole at z₀.

Equations

• residueAt f z₀ = (nhdsWithin 0 (Set.Ioi 0)).limUnder fun (r : ℝ) => (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (z : ℂ) in C(z₀, r), f z

theorem residueSimplePole_eq_of_decomposition (f : ℂ → ℂ) (z₀ c : ℂ) (g : ℂ → ℂ) (hg : AnalyticAt ℂ g z₀) (hf_eq : ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = c / (z - z₀) + g z) : residueSimplePole f z₀ = c

If f has a simple pole at z₀ with decomposition c / (z - z₀) + g, then residueSimplePole f z₀ = c.

theorem residueAt_eq_residueSimplePole (f : ℂ → ℂ) (z₀ : ℂ) (hf : HasSimplePoleAt f z₀) : residueAt f z₀ = residueSimplePole f z₀

For simple poles, residueAt agrees with residueSimplePole.

Helper lemmas for the higher-order theorem

These lemmas establish properties of the "pure residue function" f_res(z) = Σ_{s ∈ S0} c(s) / (z - s), which is used to reduce the higher-order residue theorem to the simple-pole case.

theorem hasSimplePoleAt_sum_div_sub (S0 : Finset ℂ) (c : ℂ → ℂ) (s : ℂ) (hs : s ∈ S0) : HasSimplePoleAt (fun (z : ℂ) => ∑ s' ∈ S0, c s' / (z - s')) s

The sum ∑ s ∈ S0, c(s) / (z - s) has a simple pole at each s ∈ S0, with coefficient c(s) and analytic remainder ∑ s' ∈ S0.erase s, c(s') / (z - s').

theorem differentiableOn_sum_div_sub (S0 : Finset ℂ) (c : ℂ → ℂ) (U : Set ℂ) : DifferentiableOn ℂ (fun (z : ℂ) => ∑ s ∈ S0, c s / (z - s)) (U \ ↑S0)

The sum ∑ s ∈ S0, c(s) / (z - s) is differentiable on U \ S0.

theorem residueSimplePole_sum_div_sub (S0 : Finset ℂ) (c : ℂ → ℂ) (s : ℂ) (hs : s ∈ S0) : residueSimplePole (fun (z : ℂ) => ∑ s' ∈ S0, c s' / (z - s')) s = c s

The residue of ∑ s ∈ S0, c(s) / (z - s) at s equals c(s). This follows from the HasSimplePoleAt decomposition.

theorem continuousAt_sum_remainder (S0 : Finset ℂ) (c : ℂ → ℂ) (s : ℂ) (hs : s ∈ S0) : ContinuousAt (fun (z : ℂ) => ∑ s' ∈ S0, c s' / (z - s') - residueSimplePole (fun (z : ℂ) => ∑ s' ∈ S0, c s' / (z - s')) s / (z - s)) s

ContinuousAt of the remainder (∑ c(s')/(z-s')) - c(s)/(z-s) at s. This is the hf_ext condition needed by the simple-pole theorem.

theorem cpv_eq_of_cancel_and_exists (S0 : Finset ℂ) (f f_res : ℂ → ℂ) (γ : PiecewiseC1Immersion) (hCancel : Filter.Tendsto (fun (ε : ℝ) => (∫ (t : ℝ) in γ.a..γ.b, cauchyPrincipalValueIntegrandOn S0 f γ.toFun ε t) - ∫ (t : ℝ) in γ.a..γ.b, cauchyPrincipalValueIntegrandOn S0 f_res γ.toFun ε t) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (h_res_exists : CauchyPrincipalValueExistsOn S0 f_res γ.toFun γ.a γ.b) : cauchyPrincipalValueOn S0 f γ.toFun γ.a γ.b = cauchyPrincipalValueOn S0 f_res γ.toFun γ.a γ.b

CPV(f) = CPV(f_res) when the PV difference M_f(ε) - M_res(ε) tends to 0 and the PV of f_res exists. This is the limit-arithmetic core of the higher-order reduction.

theorem generalizedResidueTheorem_higher_order_tendsto (S0 : Finset ℂ) (f : ℂ → ℂ) (γ : PiecewiseC1Immersion) (hHigherOrderCancel : Filter.Tendsto (fun (ε : ℝ) => (∫ (t : ℝ) in γ.a..γ.b, cauchyPrincipalValueIntegrandOn S0 f γ.toFun ε t) - ∫ (t : ℝ) in γ.a..γ.b, cauchyPrincipalValueIntegrandOn S0 (fun (z : ℂ) => ∑ s ∈ S0, residueAt f s / (z - s)) γ.toFun ε t) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (hPV_res_tendsto : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in γ.a..γ.b, cauchyPrincipalValueIntegrandOn S0 (fun (z : ℂ) => ∑ s ∈ S0, residueAt f s / (z - s)) γ.toFun ε t) (nhdsWithin 0 (Set.Ioi 0)) (nhds (2 * ↑Real.pi * Complex.I * ∑ s ∈ S0, generalizedWindingNumber' γ.toFun γ.a γ.b s * residueAt f s))) : 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))

Theorem (Higher-order, Tendsto formulation): Variant of generalizedResidueTheorem_higher_order with a Tendsto conclusion, taking PV convergence of the pure residue function as a hypothesis rather than deriving it from C² regularity. This avoids the hC2_cross and h_cont_deriv_cross hypotheses.

Proof: Write M_f(ε) = (M_f(ε) - M_res(ε)) + M_res(ε). The first summand tends to 0 by hHigherOrderCancel, the second to the residue sum by hPV_res_tendsto.