On-Curve PV: Endpoint and Corner CPV

Cauchy principal value existence at the endpoint 1/2 + H*I and corner -1/2 + H*I of the fundamental domain boundary fdBoundaryH H.

theorem cpv_at_endpoint (H : ℝ) (hH : √3 / 2 < H) : CauchyPrincipalValueExists' (fun (z : ℂ) => (z - (1 / 2 + ↑H * Complex.I))⁻¹) (fdBoundaryH H) 0 5 (1 / 2 + ↑H * Complex.I)

theorem cpv_at_corner (H : ℝ) (hH : √3 / 2 < H) : CauchyPrincipalValueExists' (fun (z : ℂ) => (z - (-(1 / 2) + ↑H * Complex.I))⁻¹) (fdBoundaryH H) 0 5 (-(1 / 2) + ↑H * Complex.I)