The real part of a principal-value winding number

Hungerbühler--Wasem Proposition 2.3 replaces the singular complex index integrand along a curve through w by the real integrand

((γ - w)⁻¹ * γ').im = (x y' - y x') / (x² + y²).

The complex integral generally exists only as a Cauchy principal value. By contrast, once the real integrand is interval-integrable, deleting the part of the curve inside an ε-ball about w does not change its limiting integral. This file identifies the imaginary part of the complex principal value with that ordinary real integral. After the normalization by (2πi)⁻¹, this is exactly the real part of the generalized winding number.

The result is the analytic bridge needed by the on-curve form of HW Proposition 2.3: the geometric part of that proposition supplies integrability (from boundedness at the finitely many crossings), while the remaining assertion that the principal value is purely imaginary upgrades the real-part identity here to the full real winding formula.

Main results

• HasCauchyPVAt.im_eq_integral_realWindingIntegrand identifies the imaginary part of the Cauchy-kernel principal value with the ordinary integral of realWindingIntegrand.
• windingNumber_re_eq_real_integral gives the corresponding formula for the real part of the generalized winding number.

References

• N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997 (2018), Proposition 2.3.

theorem TauCeti.Contour.HasCauchyPVAt.im_eq_integral_realWindingIntegrand {γ : ℝ → ℂ} {a b : ℝ} {w L : ℂ} (h : HasCauchyPVAt γ a b (fun (z : ℂ) => (z - w)⁻¹) w L) (h_int : IntervalIntegrable (fun (t : ℝ) => realWindingIntegrand (γ t - w) (deriv γ t)) MeasureTheory.volume a b) : L.im = ∫ (t : ℝ) in a..b, realWindingIntegrand (γ t - w) (deriv γ t)

The imaginary part of a Cauchy principal value of the index integral is the ordinary integral of the real winding integrand, provided that real integrand is interval-integrable. This remains valid when the curve passes through w: both truncations delete the same ε-ball, and dominated convergence restores the point values at crossings, where realWindingIntegrand 0 v = 0.

theorem TauCeti.Contour.windingNumber_re_eq_real_integral {γ : ℝ → ℂ} {a b : ℝ} {w : ℂ} (h : CauchyPVExistsAt γ a b (fun (z : ℂ) => (z - w)⁻¹) w) (h_int : IntervalIntegrable (fun (t : ℝ) => realWindingIntegrand (γ t - w) (deriv γ t)) MeasureTheory.volume a b) : (windingNumber γ a b w).re = 1 / (2 * Real.pi) * ∫ (t : ℝ) in a..b, realWindingIntegrand (γ t - w) (deriv γ t)

The on-curve real-integral identity for the real part of the winding number. If the Cauchy principal value defining windingNumber γ a b w exists and its real winding integrand is interval-integrable, then

(windingNumber γ a b w).re = (1 / 2π) ∫ realWindingIntegrand (γ - w) γ'.

No avoidance hypothesis is imposed, so the curve may pass through w.