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.

theorem GeneralizedResidueTheory.cpv_exists_inv_sub_of_closed_unique.cpv_of_exp_tendsto_slitPlane (R : ℝ → ℂ) (L₀ : ℂ) (δ : ℝ) (hδ : 0 < δ) (hsp : L₀ ∈ Complex.slitPlane) (h_exp : Filter.Tendsto (fun (ε : ℝ) => Complex.exp (R ε)) (nhdsWithin 0 (Set.Ioi 0)) (nhds L₀)) (hR_cont : ContinuousOn R (Set.Ioo 0 δ)) : ∃ (L : ℂ), Filter.Tendsto R (nhdsWithin 0 (Set.Ioi 0)) (nhds L)

theorem GeneralizedResidueTheory.cpv_exists_inv_sub_of_closed_unique.cpv_of_exp_tendsto_neg_slitPlane (R : ℝ → ℂ) (L₀ : ℂ) (δ : ℝ) (hδ : 0 < δ) (hsp : -L₀ ∈ Complex.slitPlane) (h_exp : Filter.Tendsto (fun (ε : ℝ) => Complex.exp (R ε)) (nhdsWithin 0 (Set.Ioi 0)) (nhds L₀)) (hR_cont : ContinuousOn R (Set.Ioo 0 δ)) : ∃ (L : ℂ), Filter.Tendsto R (nhdsWithin 0 (Set.Ioi 0)) (nhds L)