The real bounded-integrand formula for the winding number, allowing crossings

Hungerbühler–Wasem Proposition 2.3 evaluates the generalized winding number by the real, non-principal-value integral

n_s(γ) = (1 / 2π) ∫_a^b (x ẏ - y ẋ) / (x² + y²) dt, x + i y = γ - s,

for a closed piecewise-C¹ immersion γ. Winding.RealIntegral.Basic proves this when γ avoids s throughout, where the winding number is already a genuine integer. This file drops that avoidance hypothesis: s may be a value of γ, so long as every parameter where γ meets s is interior to [a, b] and derivWithin γ is Lipschitz on a one-sided closed piece ending or starting there (C^{1,1}, possibly a different piece on each side, so a crossing may coincide with a breakpoint of the immersion). The generalized winding number is then a genuine Cauchy principal value rather than an ordinary index integral, and this theorem shows it is still real and equal to the same bounded real integral. Unlike the avoiding case, interval-integrability of that integral is not assumed here: it follows from a.e. strong measurability together with the boundedness above, but the two draw from different sources -- measurability from γ's continuity plus Mathlib's unconditional measurability of deriv (aestronglyMeasurable_deriv), no different from the avoiding case; boundedness alone from the C^{1,1} crossing regularity this file's boundedness result needs. (That regularity hypothesis is satisfied vacuously when γ never meets s, so this also recovers the avoiding case for piecewise-C¹ immersions — but Winding.RealIntegral.Basic's theorem remains needed for avoiding curves that are not immersions, since it only assumes continuity, differentiability off a countable set, avoidance, and integrability; the two are kept as separate theorems, with incomparable hypotheses.)

This bundles two independent facts about the single-point Cauchy principal value L := 2πi · n_s(γ) of the Cauchy kernel (z - s)⁻¹ along γ:

• Reality (Re L = 0): the real part of the truncated index integral telescopes to Real.log ‖γ b - s‖ - Real.log ‖γ a - s‖ regardless of any branch-cut/slit-plane data — the real part of Complex.log never depends on a branch — and this vanishes by closedness.
• The integral identity (Im L = ∫ h, h the real winding integrand): supplied directly by HasCauchyPVAt.im_eq_integral_realWindingIntegrand, since h is interval-integrable.

Both facts are read off the same explicit principal-value witness, built by Crossing.PVAggregation's per-window aggregation from the plain (avoiding) pieces and the per-crossing windows along the sorted crossing list.

Main results

• TauCeti.Contour.windingNumber_eq_real_integral_of_closed_interior_crossings — the real bounded-integrand formula for a closed immersion that avoids s at its basepoint (so every crossing of s, if any, is automatically interior).
• TauCeti.Contour.isBounded_image_realWindingIntegrand_of_interior_crossings and TauCeti.Contour.intervalIntegrable_realWindingIntegrand_of_interior_crossings — the boundedness and interval-integrability facts the formula above is built from, for callers that need those facts rather than just the equality.

Provenance

New assembly of HW Prop 2.3, built from existing Tau Ceti contour-integration infrastructure: the per-crossing window value (exists_radius_perWindow_tendsto_log_norm_add_arg), the existence-and-real-part aggregation (exists_hasCauchyPVAt_re_eq_of_perWindow_tendsto_of_interiorDisjoint), the integral-identity bridge (HasCauchyPVAt.im_eq_integral_realWindingIntegrand), and the plain-piece log-norm telescoping (Winding.SegmentSum.re_integral_inv_sub_mul_deriv_eq_log_norm), which feeds the real-part telescoping hypothesis of the aggregation theorem. This file's own content is deriving the real winding integrand's boundedness and interval-integrability from the crossing regularity rather than assuming them, via Winding.LipschitzBoundedIntegrand's one-sided bounds instantiating Crossing.Windows's generic sorted-crossing-list gluing induction (sorted_crossing_gluing_induction) with that integrability invariant directly, the same way Crossing.PVAggregation's own per-window aggregation theorems instantiate it for their value-carrying invariants, rather than re-deriving the induction shape by hand -- and the assembly of all of the above into the final formula. The per-crossing window value this file reads off (exists_radius_perWindow_tendsto_log_norm_add_arg), with both its real and imaginary parts, is proved once, generically, in InvSubCPVExistence.

References

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

Interval-integrability of the real winding integrand, allowing crossings

Assembly

theorem TauCeti.Contour.isBounded_image_realWindingIntegrand_of_interior_crossings {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} (h_imm : IsPwC1ImmersionOn γ a b) (h_interior : ∀ t ∈ Set.uIcc a b, γ t = s → t ∈ Set.Ioo (min a b) (max a b)) (hγ_lip : ∀ t ∈ Set.uIcc a b, γ t = s → HasLipschitzDerivOnEachSideAt γ t) : Bornology.IsBounded ((fun (t : ℝ) => realWindingIntegrand (γ t - s) (deriv γ t)) '' Set.uIcc a b)

The real winding integrand is bounded on all of [[a, b]] for an immersion with interior crossings (Hungerbühler–Wasem Prop 2.3, boundedness half). Needs no closedness, only that every crossing of s is interior to [[a, b]]. Orientation-generic, like IsPwC1ImmersionOn itself: no a ≤ b is needed. See windingNumber_eq_real_integral_of_closed_interior_crossings below for the closed-curve equality and the full documentation of hγ_lip.

theorem TauCeti.Contour.intervalIntegrable_realWindingIntegrand_of_interior_crossings {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} (h_imm : IsPwC1ImmersionOn γ a b) (h_interior : ∀ t ∈ Set.uIcc a b, γ t = s → t ∈ Set.Ioo (min a b) (max a b)) (hγ_lip : ∀ t ∈ Set.uIcc a b, γ t = s → HasLipschitzDerivOnEachSideAt γ t) : IntervalIntegrable (fun (t : ℝ) => realWindingIntegrand (γ t - s) (deriv γ t)) MeasureTheory.volume a b

The real winding integrand is interval-integrable along an immersion with interior crossings (Hungerbühler–Wasem Prop 2.3, integrability half). Needs no closedness, only that every crossing of s is interior to [[a, b]]. Orientation-generic, like IsPwC1ImmersionOn itself: no a ≤ b is needed. See windingNumber_eq_real_integral_of_closed_interior_crossings below for the closed-curve equality and the full documentation of hγ_lip.

theorem TauCeti.Contour.windingNumber_eq_real_integral_of_closed_interior_crossings {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} (h_imm : IsPwC1ImmersionOn γ a b) (hclosed : γ a = γ b) (hsa : γ a ≠ s) (hγ_lip : ∀ t ∈ Set.uIcc a b, γ t = s → HasLipschitzDerivOnEachSideAt γ t) : windingNumber γ a b s = ↑(1 / (2 * Real.pi) * ∫ (t : ℝ) in a..b, realWindingIntegrand (γ t - s) (deriv γ t))

The real bounded-integrand formula, allowing crossings (Hungerbühler–Wasem Prop 2.3). For a closed piecewise-C¹ immersion γ on [[a, b]] that avoids s at the basepoint a (hsa, so also at b by closedness — every other crossing of s, if any, is automatically interior to [[a, b]]) and is C^{1,1} on each side of any such crossing (derivWithin γ Lipschitz on a one-sided closed piece ending or starting there, hγ_lip — the two sides need not agree, so a crossing may coincide with a breakpoint of the immersion) — in particular satisfied vacuously if γ never meets s — the generalized winding number n_s(γ) is a real number equal to its ordinary (non-principal-value) integral:

n_s(γ) = (1 / 2π) ∫_a^b (x ẏ - y ẋ) / (x² + y²) dt, x + i y = γ - s.

The two sides of a crossing need not agree: hγ_lip allows the crossing to coincide with a breakpoint of the piecewise-C¹ immersion (a corner), matching Hungerbühler–Wasem's own proof of Prop 2.3, which handles that case via the same one-sided splitting (arXiv:1808.00997, p. 9). Orientation-generic, like windingNumber and intervalIntegral themselves: no a ≤ b is needed.