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_of_interiorDisjoint).

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].
• Contour.exists_radius_perWindow_tendsto_log_norm_add_arg — the same per-window convergence, but with the limit's explicit log-norm-plus-argument value exposed rather than only its existence, for callers (the on-curve real-integral formula) that need the limit's real or imaginary part, not just that it exists.

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.exists_radius_perWindow_tendsto_log_norm_add_arg {γ : ℝ → ℂ} {a b t₀ : ℝ} {s : ℂ} (h_imm : IsPwC1ImmersionOn γ a b) (ht₀ : t₀ ∈ Set.Ioo a b) (h_at : γ t₀ = s) : ∃ R > 0, ∃ (L_R : ℂ) (L_L : ℂ), L_R ≠ 0 ∧ L_L ≠ 0 ∧ Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds L_R) ∧ Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Iio t₀)) (nhds L_L) ∧ ∀ (l u : ℝ), t₀ - R ≤ l → l < t₀ → t₀ < u → u ≤ t₀ + R → a < l → u ≤ b → (∀ t ∈ Set.Icc l u, γ t = s → t = t₀) → Filter.Tendsto (fun (ε : ℝ) => ∫ (v : ℝ) in l..u, if ‖γ v - s‖ > ε then (γ v - s)⁻¹ * deriv γ v else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds (↑(Real.log ‖γ u - s‖ - Real.log ‖γ l - s‖) + ↑((-L_L / (γ l - s)).arg + ((γ u - s) / L_R).arg) * Complex.I))

Value-exposing form of the per-crossing window radius. Around each interior crossing there is a radius R > 0 and the crossing's nonzero one-sided tangent limits L_R, L_L of deriv γ (from the right and left respectively — hL_tend_R, hL_tend_L pin them down, so a caller can compute with the value below rather than treat L_R, L_L as opaque), such that at every window [l, u] ⊆ [t₀ - R, t₀ + R] that lies inside [a, b] and contains no other crossing, the truncated window integral of the Cauchy kernel converges to that explicit log-norm-plus-argument value (the value perWindow_truncated_integral_tendsto supplies), rather than to a merely existentially-bound limit. A consumer that only needs existence of the limit (not its value) can take the displayed value itself as the existential witness, so no separate existence-only wrapper is kept here.

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.