The principal value of a polar part is the winding-weighted residue

For a piecewise-C¹ immersed closed curve whose crossings of a pole s ∈ S are interior and, at every surviving higher-order coefficient, flat and sector-compatible, the single-point Cauchy principal value of the polar part of f at s along the curve is 2πi · n_s(γ) · Res_s f — the term s contributes to the Hungerbühler–Wasem sum. The simple-pole coefficient contributes its winding-weighted residue by the definitional identity windingNumber = (2πi)⁻¹ · cauchyPVAt together with the existence theorem (Contour.IsPwC1ImmersionOn.cauchyPVExistsAt_inv_sub); every order-k ≥ 2 coefficient contributes zero around a closed curve (Contour.IsPwC1ImmersionOn.hasCauchyPVAt_pow_inv); the finite Laurent sum assembles by ℂ-linearity, and the leading coefficient is the residue (Contour.PolarPartDecomposition.residue_eq).

Main results

• Contour.PolarPartDecomposition.hasCauchyPVAt_polarPart — the single-point principal value of the polar part at s along a closed immersion is 2πi · windingNumber · residue.

Provenance

Migrated from cpv_polarPart_at_multiCrossed_pole_under_condB_corner of MultiCrossingCPV.lean in the AINTLIB LeanModularForms development, restated for a raw curve: the simple-pole principal value is derived from the immersion rather than assumed, and the sector hypothesis quantifies over the one-sided derivative limits (which are unique) instead of chosen tangent functions. See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3.

theorem TauCeti.Contour.PolarPartDecomposition.hasCauchyPVAt_polarPart {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} (decomp : PolarPartDecomposition f S U) (s : ↥S) {γ : ℝ → ℂ} {a b : ℝ} (h_imm : IsPwC1ImmersionOn γ a b) (hab : a ≤ b) (hclosed : γ a = γ b) (h_interior : ∀ t ∈ Set.Icc a b, γ t = ↑s → t ∈ Set.Ioo a b) (h_flat : ∀ (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 : ∀ (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) : HasCauchyPVAt γ a b (decomp.polarPart s) (↑s) (2 * ↑Real.pi * Complex.I * windingNumber γ a b ↑s * residue f ↑s)

The principal value of a polar part is the winding-weighted residue: along a closed piecewise-C¹ immersion whose crossings of s are interior and, at every surviving higher-order coefficient, flat and sector-compatible, the single-point Cauchy principal value of decomp.polarPart s at s is 2πi · n_s(γ) · Res_s f. The higher-order coefficients contribute nothing — this is the term the Hungerbühler–Wasem sum attributes to s.