On-Curve PV: Main Theorem

For any point s on fdBoundaryH H, the CPV integral of (z - s)⁻¹ exists.

Helper: s = I, H ≤ 1, H < 1

Helper: s = I, H = 1

Helper: generic case, t₀ on seg1 (0 < t₀ < 1)

Helper: generic case, t₀ on arc (1 < t₀ < 3) with seg5 crossing

Helper: generic case, t₀ on arc (1 < t₀ < 3) without seg5 crossing

Helper: generic case, t₀ on arc (1 < t₀ < 3), dispatches to cross/no-cross

Helper: generic case, t₀ on seg4 (3 < t₀ < 4)

Helper: generic case, t₀ on seg5 (4 < t₀ < 5) with normSq = 1

Helper: generic case, t₀ on seg5 (4 < t₀ < 5) without normSq = 1

Helper: generic case, t₀ on seg5 (4 < t₀ < 5), dispatches

Main theorem

theorem fdBoundary_H_cpv_exists_of_onCurve (H : ℝ) (hH : √3 / 2 < H) (s : ℂ) (h_on : ∃ t ∈ Set.Icc 0 5, fdBoundaryH H t = s) : CauchyPrincipalValueExists' (fun (z : ℂ) => (z - s)⁻¹) (fdBoundaryH H) 0 5 s

For any point on fdBoundaryH H, the CPV integral of (z - s)⁻¹ exists.