Assembling the generalized residue sum

The engine of the Hungerbühler–Wasem generalized residue theorem, over an explicit polar decomposition: along a closed 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 the ordinary contour integral of the analytic remainder plus 2πi · Σ_{s ∈ S} n_s(γ) · Res_s f. 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.

Null-homology enters only at the last step, where it makes the analytic remainder integrate to zero (the homology Cauchy theorem through the decomposition). Keeping that step separate is what lets a caller add several curves up before any of them bounds, as the cycle form of the generalized residue theorem must.

Main results

• Contour.PolarPartDecomposition.hasCauchyPV_analyticRemainder_add_residue_sum — the null-homology-free splitting: the principal value is the contour integral of the analytic remainder plus 2πi · Σ_{s ∈ S} n_s(γ) · Res_s f.
• 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_analyticRemainder_add_residue_sum {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} (decomp : PolarPartDecomposition f S U) {γ : ℝ → ℂ} {a b : ℝ} (h_imm : IsPwC1ImmersionOn γ a b) (hab : a ≤ b) (hclosed : γ a = γ b) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ 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 ((∫ (t : ℝ) in a..b, deriv γ t • decomp.analyticRemainder (γ t)) + 2 * ↑Real.pi * Complex.I * ∑ s ∈ S, windingNumber γ a b s * residue f s)

The residue sum splits off the principal value over a polar decomposition: along a closed 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 the ordinary contour integral of the analytic remainder plus 2πi · Σ_{s ∈ S} n_s(γ) · Res_s f.

Nothing is assumed about null-homology, so the identity holds for a single immersion however it winds around the holes of U. That is what makes it usable one rung lower down, where the remainder is discharged only after the contributions of several curves have been added up: over a formal cycle whose generators need not individually bound (TauCeti.Contour.Cycle.hungerbuhlerWasem_residueTheorem).

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.

The null-homology-free splitting (Contour.PolarPartDecomposition.hasCauchyPV_analyticRemainder_add_residue_sum) with the analytic remainder discharged by the homology Cauchy theorem.