PV Integral Splitting at Crossings

For a curve γ with a unique crossing of point s at parameter t₀, the PV cutoff integral splits into left and right pieces — the near-crossing part vanishes.

The key observation: when ‖γ(t) - s‖ ≤ ε (i.e., t is near the crossing), the cutoff integrand if ‖γ t - s‖ > ε then (γ t - s)⁻¹ * deriv γ t else 0 is 0. On the far segments, the cutoff condition is satisfied so the integrand equals (γ t - s)⁻¹ * deriv γ t a.e.

Main results

• pv_split_at_crossing — the PV cutoff integral equals the sum of left and right integrals of (γ t - s)⁻¹ * deriv γ t, where the middle part is zero.

theorem ContourIntegral.pv_split_at_crossing {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} {ε δ t₀ : ℝ} (_hab : a < b) (ht₀ : t₀ ∈ Set.Ioo a b) (_hε : 0 < ε) (hδ : 0 < δ) (hδ_small : δ < min (t₀ - a) (b - t₀)) (h_far : ∀ t ∈ Set.Icc a b, δ < |t - t₀| → ε < ‖γ t - s‖) (h_near : ∀ (t : ℝ), |t - t₀| ≤ δ → ‖γ t - s‖ ≤ ε) (hint_left : IntervalIntegrable (fun (t : ℝ) => (γ t - s)⁻¹ * deriv γ t) MeasureTheory.volume a (t₀ - δ)) (hint_right : IntervalIntegrable (fun (t : ℝ) => (γ t - s)⁻¹ * deriv γ t) MeasureTheory.volume (t₀ + δ) b) : (∫ (t : ℝ) in a..b, if ‖γ t - s‖ > ε then (γ t - s)⁻¹ * deriv γ t else 0) = (∫ (t : ℝ) in a..t₀ - δ, (γ t - s)⁻¹ * deriv γ t) + ∫ (t : ℝ) in t₀ + δ..b, (γ t - s)⁻¹ * deriv γ t

The PV cutoff integral splits at a crossing.

For ε, δ > 0 with δ < min(t₀ - a, b - t₀), if:

• the curve is far from s (norm > ε) outside the δ-window, and
• near to s (norm ≤ ε) inside the δ-window,

then the full cutoff integral equals the sum of the left and right integrals of (γ t - s)⁻¹ * deriv γ t. The middle piece vanishes because the cutoff sets the integrand to 0 whenever ‖γ t - s‖ ≤ ε.