Winding Number Weight at i

PV integral computation and generalized winding number of fdBoundaryH around the point i.

Main Results

• pv_integral_at_i_tendsto — PV integral converges to -iπ
• gWN_fdBoundary_H_at_i — gWN = -1/2 at i

theorem pv_integral_at_i_tendsto (H : ℝ) (hH : 1 < H) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in 0..5, if ‖fdBoundaryH H t - Complex.I‖ > ε then (fdBoundaryH H t - Complex.I)⁻¹ * deriv (fun (s : ℝ) => fdBoundaryH H s - Complex.I) t else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds (-(Complex.I * ↑Real.pi)))

The PV integral of (γ-I)⁻¹ γ' over [0,5] with ε-ball cutoff tends to -iπ.

Proof wires through pv_tendsto_of_crossing_limit with:

• t₀ = 2 (arc crossing at i)
• δ(ε) = 12/π · arcsin(ε/2) (arc-length inverse of the norm formula)
• E(ε) = log(g(2-δ)) - log(g(2+δ)) - 2πi (FTC telescope with branch correction)
• h_limit : E(ε) → -(I·π) (arg computation shows the difference is constantly -iπ)

theorem gWN_fdBoundary_H_at_i (H : ℝ) (hH : 1 < H) : generalizedWindingNumber' (fdBoundaryH H) 0 5 Complex.I = -1 / 2

generalizedWindingNumber' (fdBoundaryH H) 0 5 I = -1/2.

Note: requires 1 < H (not just √3/2 < H) because for H > 1, the point I is strictly inside the contour and the branch cut correction on seg 3 contributes -2πi. For √3/2 < H < 1, I would be outside the contour and the result would be +1/2.