CPV Existence for Inverse along Piecewise C¹ Immersions

CPV existence for (z-z₀)⁻¹ along closed piecewise C¹ immersions with a unique crossing point. This is infrastructure needed by both the convex and null-homologous residue theorems.

Main results

• cpv_exists_inv_sub_of_closed_unique: CPV of (z-z₀)⁻¹ exists for closed curves with a unique crossing through z₀.

theorem GeneralizedResidueTheory.cpv_exists_inv_sub_of_closed_unique (γ : PiecewiseC1Immersion) (z₀ : ℂ) (hclosed : γ.IsClosed) (_h_no_endpt : γ.toFun γ.a ≠ z₀ ∧ γ.toFun γ.b ≠ z₀) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = z₀) (honly : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t = z₀ → t = t₀) : CauchyPrincipalValueExists' (fun (z : ℂ) => (z - z₀)⁻¹) γ.toFun γ.a γ.b z₀

PV of (z-z₀)⁻¹ exists along a closed PiecewiseC1Immersion with unique crossing. This is the C²-free version of cpv_exists_inv_sub: it uses the exp-convergence from tendsto_exp_cutoff_integral_crossing (which doesn't need C²) together with a Cauchy transfer argument to extract convergence of the integral itself.