Winding Number Weight at ρ+1

PV integral computation and generalized winding number of fdBoundaryH around the elliptic point ρ+1 = e^{πi/3}.

Main Results

• pv_integral_at_rho_plus_one_tendsto — PV integral converges to -iπ/3
• gWN_fdBoundary_H_at_rho_plus_one — gWN = -1/6 at ρ+1

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

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

theorem gWN_fdBoundary_H_at_rho_plus_one (H : ℝ) (hH : √3 / 2 < H) : generalizedWindingNumber' (fdBoundaryH H) 0 5 ellipticPointRhoPlusOne = -1 / 6

generalizedWindingNumber' (fdBoundaryH H) 0 5 ρ' = -1/6.