Winding Number Weight at ρ

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

Main Results

• pv_integral_at_rho_tendsto — PV integral converges to -iπ/3
• gWN_fdBoundary_H_at_rho — gWN = -1/6 at ρ

theorem fdBoundary_H_sub_rho_seg0_re (H : ℝ) {t : ℝ} (ht : t ≤ 1) : (fdBoundaryH H t - ellipticPointRho).re = 1

theorem fdBoundary_H_sub_rho_seg0_slitPlane (H : ℝ) {t : ℝ} (ht : t ≤ 1) : fdBoundaryH H t - ellipticPointRho ∈ Complex.slitPlane

theorem fdBoundary_H_sub_rho_seg1_re (H : ℝ) {t : ℝ} (ht1 : 1 < t) (ht2 : t ≤ 2) : (fdBoundaryH H t - ellipticPointRho).re > 0

On seg 1: γ(t) - ρ has re = cos(θ(t)) + 1/2 where θ ∈ [π/3, π/2], so cos(θ) ∈ [0, 1/2] and re ∈ [1/2, 1] > 0.

theorem fdBoundary_H_sub_rho_seg2_re (H : ℝ) {t : ℝ} (ht2 : 2 < t) (ht3 : t < 3) : (fdBoundaryH H t - ellipticPointRho).re > 0

On seg 2 (t ∈ (2, 3)): γ(t) - ρ has re = cos(θ(t)) + 1/2 > 0 since θ ∈ (π/2, 2π/3) gives cos ∈ (-1/2, 0) hence re ∈ (0, 1/2).

theorem fdBoundary_H_sub_rho_seg3_slitPlane (H : ℝ) (hH : √3 / 2 < H) {t : ℝ} (ht3 : 3 < t) (ht4 : t ≤ 4) : fdBoundaryH H t - ellipticPointRho ∈ Complex.slitPlane

On seg 3 (t ∈ (3, 4]): γ(t) - ρ = (y(t) - √3/2)I with y > √3/2, so im > 0.

theorem fdBoundary_H_sub_rho_seg4_slitPlane (H : ℝ) (hH : √3 / 2 < H) {t : ℝ} (ht4 : 4 < t) (_ht5 : t ≤ 5) : fdBoundaryH H t - ellipticPointRho ∈ Complex.slitPlane

On seg 4: γ(t) - ρ has im = H - √3/2 > 0 for H > √3/2.

theorem fdBoundary_H_sub_rho_slitPlane (H : ℝ) (hH : √3 / 2 < H) {t : ℝ} (ht : t ∈ Set.Icc 0 5) (hne : t ≠ 3) : fdBoundaryH H t - ellipticPointRho ∈ Complex.slitPlane

Combined: γ(t) - ρ ∈ slitPlane for all t ∈ [0, 5] with t ≠ 3.

theorem fdBoundary_H_eq_rho_iff (H : ℝ) (hH : √3 / 2 < H) {t : ℝ} (ht : t ∈ Set.Icc 0 5) : fdBoundaryH H t = ellipticPointRho ↔ t = 3

ρ is only hit at t = 3.

theorem arg_approach_rho_left {H : ℝ} : Filter.Tendsto (fun (δ : ℝ) => (fdBoundaryH H (3 - δ) - ellipticPointRho).arg) (nhdsWithin 0 (Set.Ioi 0)) (nhds (Real.pi / 6))

The arg of the approach direction from the left (seg 2 side) at ρ. γ(3-δ) - ρ ≈ δ·(π/6)·exp(iπ/6), so arg → π/6.

theorem arg_approach_rho_right (H : ℝ) (hH : √3 / 2 < H) {δ : ℝ} (hδ : 0 < δ) (hδ4 : δ ≤ 1) : (fdBoundaryH H (3 + δ) - ellipticPointRho).arg = Real.pi / 2

The arg of the approach direction from the right (seg 3 side) at ρ. γ(3+δ) - ρ = δ(H-√3/2)I, so arg = π/2 (exact, not just limit).

theorem pv_integral_at_rho_tendsto (H : ℝ) (hH : √3 / 2 < H) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in 0..5, if ‖fdBoundaryH H t - ellipticPointRho‖ > ε then (fdBoundaryH H t - ellipticPointRho)⁻¹ * deriv (fun (s : ℝ) => fdBoundaryH H s - ellipticPointRho) 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 (H : ℝ) (hH : √3 / 2 < H) : generalizedWindingNumber' (fdBoundaryH H) 0 5 ellipticPointRho = -1 / 6

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