Winding Number from PV Integral Limit

Convert a Tendsto result for the PV integral into a generalized winding number value. This is the final step shared by all winding number computations.

Main results

• gWN_eq_of_pv_tendsto — general: gWN = L / (2πi) from Tendsto
• gWN_eq_neg_half_of_pv_tendsto — specialized: L = -πi implies gWN = -1/2
• gWN_eq_neg_sixth_of_pv_tendsto — specialized: L = -πi/3 implies gWN = -1/6

theorem ContourIntegral.gWN_eq_of_pv_tendsto (γ : ℝ → ℂ) (a b : ℝ) (s L : ℂ) (h : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ε < ‖γ t - s - 0‖ then (γ t - s)⁻¹ * deriv (fun (t : ℝ) => γ t - s) t else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds L)) : generalizedWindingNumber' γ a b s = L / (2 * ↑Real.pi * Complex.I)

If the PV integral of (γ(t) - s)⁻¹ · deriv(γ - s)(t) tends to L as ε → 0⁺, then generalizedWindingNumber' γ a b s = L / (2 * π * I).

theorem ContourIntegral.gWN_eq_neg_half_of_pv_tendsto (γ : ℝ → ℂ) (a b : ℝ) (s : ℂ) (h : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ε < ‖γ t - s - 0‖ then (γ t - s)⁻¹ * deriv (fun (t : ℝ) => γ t - s) t else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds (-(↑Real.pi * Complex.I)))) : generalizedWindingNumber' γ a b s = -1 / 2

Specialized version: if the PV integral tends to -(π * I), then gWN = -1/2.

theorem ContourIntegral.gWN_eq_neg_sixth_of_pv_tendsto (γ : ℝ → ℂ) (a b : ℝ) (s : ℂ) (h : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ε < ‖γ t - s - 0‖ then (γ t - s)⁻¹ * deriv (fun (t : ℝ) => γ t - s) t else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds (-(↑Real.pi / 3 * Complex.I)))) : generalizedWindingNumber' γ a b s = -1 / 6

Specialized version: if the PV integral tends to -(π / 3 * I), then gWN = -1/6.