The per-window principal value at a simple pole

At a transverse crossing γ t₀ = s with unique crossing on a window [l, u], the ε-truncated integral of the simple-pole integrand (γ t - s)⁻¹ * deriv γ t over the window converges as ε → 0⁺ (perWindow_truncated_integral_tendsto). The window integral splits at the exit times (exists_exit_times_truncated_integral_split); each side integral is the logarithm of a chord quotient by the logarithmic fundamental theorem of calculus; the log ε real parts of the two sides cancel — both exit radii are exactly ε — and the argument parts converge by the annular argument limits, so the whole expression tends to

(log ‖γ u - s‖ - log ‖γ l - s‖) + (arg_R + arg_L) · I.

The slit-plane hypotheses are taken as inputs rather than derived internally — the caller fixes the window radius once (for multi-crossing aggregation each crossing supplies a threshold radius and the minimum is used). The chord-quotient inputs are produced by Contour.exists_chord_quotient_mem_slitPlane_right/left; the tangent-side inputs are supplied externally by the window-boundary radii.

Main results

• Contour.perWindow_truncated_integral_tendsto — the truncated window integral of the simple-pole integrand converges as ε → 0⁺, to the log-norm difference of the window boundary plus the boundary arguments.

Provenance

Migrated from perCrossing_window_integral_tendsto_exact and its supporting lemmas (annular_log_diff_of_window, right/left_annular_log_diff_local, log_div_re_im_decomp) of LocalCutoffs.lean in the AINTLIB LeanModularForms development, restated for a raw curve on its crossing window. The truncated-integrability lemma migrated alongside them, cpvIntegrand_inv_intervalIntegrable, lives with the rest of the truncation API in Contour.Cauchy.PrincipalValue.Basic as intervalIntegrable_inv_sub_truncated. See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3.

theorem TauCeti.Contour.perWindow_truncated_integral_tendsto {γ : ℝ → ℂ} {s : ℂ} {l t₀ u : ℝ} {L_R L_L : ℂ} {P : Set ℝ} (hlt : l < t₀) (htu : t₀ < u) (h_at : γ t₀ = s) (hγ_cont : ContinuousOn γ (Set.Icc l u)) (h_tendsto_R : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds L_R)) (h_tendsto_L : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Iio t₀)) (nhds L_L)) (h_diff_R : ∀ᶠ (t : ℝ) in nhdsWithin t₀ (Set.Ioi t₀), DifferentiableAt ℝ γ t) (h_diff_L : ∀ᶠ (t : ℝ) in nhdsWithin t₀ (Set.Iio t₀), DifferentiableAt ℝ γ t) (hP : P.Countable) (hγ_diffP : ∀ t ∈ Set.Ioo l u \ P, DifferentiableAt ℝ γ t) (hderiv_int : IntervalIntegrable (fun (t : ℝ) => deriv γ t) MeasureTheory.volume l u) (h_unique : ∀ t ∈ Set.Icc l u, γ t = s → t = t₀) (h_slit_R : ∀ (a b : ℝ), t₀ < a → a ≤ b → b ≤ u → (γ b - s) / (γ a - s) ∈ Complex.slitPlane) (h_slit_L : ∀ (b : ℝ), l ≤ b → b < t₀ → (γ b - s) / (γ l - s) ∈ Complex.slitPlane) (h_slit_plus : (γ u - s) / L_R ∈ Complex.slitPlane) (h_slit_minus : -L_L / (γ l - s) ∈ Complex.slitPlane) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in l..u, if ‖γ t - s‖ > ε then (γ t - s)⁻¹ * deriv γ t 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))

The per-window principal value at a simple pole: at a transverse crossing γ t₀ = s with unique crossing on the window, non-zero one-sided derivative limits, and the slit-plane inputs at the window radius, the ε-truncated window integral of (γ t - s)⁻¹ * deriv γ t converges as ε → 0⁺ to the log-norm difference of the window boundary plus the two boundary arguments.