Assembling the generalized residue sum

The engine of the Hungerbühler–Wasem generalized residue theorem, over an explicit polar decomposition: along a closed, null-homologous piecewise-C¹ immersion in U whose crossings of each pole are interior and (at every surviving higher-order coefficient) flat and sector-compatible, the set-level Cauchy principal value of f exists and equals 2πi · Σ_{s ∈ S} n_s(γ) · Res_s f. The analytic remainder integrates to zero around the null-homologous cycle (the homology Cauchy theorem through the decomposition), each polar part contributes its winding-weighted residue, the contributions add across the singular set, and f is identified with the assembled sum along the curve away from the poles — which is all the excised principal value sees.

Main results

• Contour.PolarPartDecomposition.hasCauchyPV_residue_sum — the set-level principal value of f along the cycle is 2πi · Σ_{s ∈ S} n_s(γ) · Res_s f.

Provenance

Migrated from residueTheorem_crossing_compositional of Crossing.lean in the AINTLIB LeanModularForms development (there taking the per-pole principal values as data; here they are produced by the polar-part theorem). See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3.

theorem TauCeti.Contour.PolarPartDecomposition.hasCauchyPV_residue_sum {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} (decomp : PolarPartDecomposition f S U) (hU : IsOpen U) {γ : ℝ → ℂ} {a b : ℝ} (h_imm : IsPwC1ImmersionOn γ a b) (hab : a ≤ b) (hclosed : γ a = γ b) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hnull : IsNullHomologous γ a b U) (h_interior : ∀ (s : ↥S), ∀ t ∈ Set.Icc a b, γ t = ↑s → t ∈ Set.Ioo a b) (h_flat : ∀ (s : ↥S) (k : Fin (decomp.order s)), 1 ≤ ↑k → decomp.coeff s k ≠ 0 → ∀ t ∈ Set.Icc a b, γ t = ↑s → FlatOfOrder γ t (↑k + 1)) (h_B : ∀ (s : ↥S) (k : Fin (decomp.order s)), 1 ≤ ↑k → decomp.coeff s k ≠ 0 → ∀ t ∈ Set.Icc a b, γ t = ↑s → ∀ (L_R L_L : ℂ), Filter.Tendsto (deriv γ) (nhdsWithin t (Set.Ioi t)) (nhds L_R) → Filter.Tendsto (deriv γ) (nhdsWithin t (Set.Iio t)) (nhds L_L) → (L_R / ↑‖L_R‖) ^ ↑k = (-L_L / ↑‖L_L‖) ^ ↑k) : HasCauchyPV γ a b f (2 * ↑Real.pi * Complex.I * ∑ s ∈ S, windingNumber γ a b s * residue f s)

The generalized residue sum over a polar decomposition: along a closed, null-homologous piecewise-C¹ immersion in U whose crossings of each pole are interior and gated-flat and gated-sector-compatible, the set-level principal value of f is 2πi · Σ_{s ∈ S} n_s(γ) · Res_s f.