Existence of the Cauchy-kernel principal value along an immersed curve

For a piecewise-C¹ immersed curve γ on [a, b] whose value-s parameters are all interior, the single-point Cauchy principal value of t ↦ (γ t - s)⁻¹ * deriv γ t exists on [a, b] — the integral defining the winding number converges even when the curve passes through s. The immersion makes the crossing set finite; each interior crossing carries a slit-plane radius (Contour.exists_crossing_slitPlane_radius), the radii shrink to a common window radius (Contour.exists_common_window_radius), each window integral converges (Contour.perWindow_truncated_integral_tendsto), and the windows aggregate (Contour.cauchyPVExistsAt_of_perWindow_tendsto).

Main results

• Contour.IsPwC1ImmersionOn.cauchyPVExistsAt_inv_sub — the single-point principal value at s of the Cauchy kernel exists along a piecewise-C¹ immersion whose crossings of s are interior to [a, b].

Provenance

Migrated from the existence content of hasCauchyPV_inv_sub_multiCrossing_corner of MultiCrossingCPV.lean in the AINTLIB LeanModularForms development (there stated for the bundled ClosedPwC1Immersion, with the per-crossing radii of exists_per_crossing_radius). See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3.

theorem TauCeti.Contour.IsPwC1ImmersionOn.cauchyPVExistsAt_inv_sub {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} (h_imm : IsPwC1ImmersionOn γ a b) (hab : a ≤ b) (h_interior : ∀ t ∈ Set.Icc a b, γ t = s → t ∈ Set.Ioo a b) : CauchyPVExistsAt γ a b (fun (z : ℂ) => (z - s)⁻¹) s

Existence of the Cauchy-kernel principal value along a piecewise-C¹ immersion: if every parameter of [a, b] where γ meets s is interior, the single-point Cauchy principal value of t ↦ (γ t - s)⁻¹ * deriv γ t at s exists on [a, b]. Endpoint crossings are excluded by h_interior; for a closed curve this is the choice of a basepoint off s.