Meromorphic Contour Integral Vanishing (Null-Homologous)

Extensions of the null-homologous Cauchy theorem to meromorphic functions. The key results show that contour integrals of meromorphic functions with zero residues vanish along null-homologous curves.

Main results

• contourIntegral_eq_zero_of_meromorphic_residue_zero_nh -- single-pole meromorphic vanishing
• contourIntegral_eq_zero_of_meromorphic_residue_zero_finset_nh -- multi-pole meromorphic vanishing (by induction on |S|)
• conditionsAB_imply_higherOrderCancel_nh -- null-homologous higher-order cancellation
• pv_res_tendsto_of_immersion_nullHomologous -- PV residue sum convergence for null-homologous curves

theorem contourIntegral_eq_zero_of_meromorphic_residue_zero_nh (f : ℂ → ℂ) (s : ℂ) (hf : MeromorphicAt f s) (hres : residueAt f s = 0) (U : Set ℂ) (hU : IsOpen U) (hf_diff : DifferentiableOn ℂ f (U \ {s})) (hs_in_U : s ∈ U) (γ : PiecewiseC1Immersion) (h_null : IsNullHomologous γ U) (hγ_avoids : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ s) : ∫ (t : ℝ) in γ.a..γ.b, f (γ.toFun t) * deriv γ.toFun t = 0

Null-homologous version: contour integral of meromorphic function with zero residue vanishes when the curve is null-homologous and avoids the singularity.

theorem contourIntegral_eq_zero_of_meromorphic_residue_zero_finset_nh (S : Finset ℂ) (f : ℂ → ℂ) (hf_mero : ∀ s ∈ S, MeromorphicAt f s) (hres : ∀ s ∈ S, residueAt f s = 0) (U : Set ℂ) (hU : IsOpen U) (hf_diff : DifferentiableOn ℂ f (U \ ↑S)) (γ : PiecewiseC1Immersion) (h_null : IsNullHomologous γ U) (hγ_avoids : ∀ s ∈ S, ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ s) : ∫ (t : ℝ) in γ.a..γ.b, f (γ.toFun t) * deriv γ.toFun t = 0

Finset version: induction on |S| using the single-pole version.

L5: Assembly — conditions (A')+(B) imply higher-order cancellation

The main result: combine per-term vanishing over all Laurent terms and all crossing points to show the global PV difference tends to 0.

Note: This uses SatisfiesConditionA' (variable-order flatness matching the pole order) rather than SatisfiesConditionA (order 1 only). The paper's Theorem 3.3 requires flatness of the pole order, which is stronger than flatness of order 1 for higher-order poles.

theorem conditionsAB_imply_higherOrderCancel_nh (U : Set ℂ) (hU : IsOpen U) (S0 : Finset ℂ) (f : ℂ → ℂ) (hf : DifferentiableOn ℂ f (U \ ↑S0)) (γ : PiecewiseC1Immersion) (h_null : IsNullHomologous γ U) (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 : ∀ 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₂) (hS0_in_U : ∀ s ∈ S0, s ∈ U) : 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)

Null-homologous version of conditionsAB_imply_higherOrderCancel.

theorem pv_res_tendsto_of_immersion_nullHomologous (U S : Set ℂ) (hS_discrete : ∀ s ∈ S, ∃ ε > 0, ∀ s' ∈ S, s' ≠ s → ε ≤ ‖s' - s‖) (hS_closed : IsClosed S) (S0 : Finset ℂ) (hS0_subset : ∀ s ∈ S0, s ∈ S) (f : ℂ → ℂ) (γ : PiecewiseC1Immersion) (h_null : IsNullHomologous γ U) (hS_on_curve : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ∈ S → γ.toFun t ∈ 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 (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))