Crossing Limit Theorem

The master theorem: for a closed piecewise C1 curve with a unique crossing at t₀, the PV integral of (γ-s)⁻¹ · γ' equals the limit of the log ratio log(g(t₀-δ)) - log(g(t₀+δ)) as δ → 0⁺.

This combines PVSplit (integral splitting) with SegmentFTC (telescoping) to reduce PV computation to a single crossing-local limit.

Main results

• pv_tendsto_of_crossing_limit — the PV integral tends to L if the log ratio at the crossing tends to L

theorem ContourIntegral.pv_tendsto_of_crossing_limit {γ : ℝ → ℂ} {a b : ℝ} {s L : ℂ} {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioo a b) {δ : ℝ → ℝ} {threshold : ℝ} (hthresh : 0 < threshold) (hδ_pos : ∀ (ε : ℝ), 0 < ε → ε < threshold → 0 < δ ε) (hδ_small : ∀ (ε : ℝ), 0 < ε → ε < threshold → δ ε < min (t₀ - a) (b - t₀)) (h_far : ∀ (ε : ℝ), 0 < ε → ε < threshold → ∀ t ∈ Set.Icc a b, δ ε < |t - t₀| → ε < ‖γ t - s‖) (h_near : ∀ (ε : ℝ), 0 < ε → ε < threshold → ∀ (t : ℝ), |t - t₀| ≤ δ ε → ‖γ t - s‖ ≤ ε) {E : ℝ → ℂ} (h_ftc : ∀ (ε : ℝ), 0 < ε → ε < threshold → (∫ (t : ℝ) in a..t₀ - δ ε, (γ t - s)⁻¹ * deriv γ t) + ∫ (t : ℝ) in t₀ + δ ε..b, (γ t - s)⁻¹ * deriv γ t = E ε) (hint_left : ∀ (ε : ℝ), 0 < ε → ε < threshold → IntervalIntegrable (fun (t : ℝ) => (γ t - s)⁻¹ * deriv γ t) MeasureTheory.volume a (t₀ - δ ε)) (hint_right : ∀ (ε : ℝ), 0 < ε → ε < threshold → IntervalIntegrable (fun (t : ℝ) => (γ t - s)⁻¹ * deriv γ t) MeasureTheory.volume (t₀ + δ ε) b) (h_limit : Filter.Tendsto E (nhdsWithin 0 (Set.Ioi 0)) (nhds L)) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ‖γ t - s‖ > ε then (γ t - s)⁻¹ * deriv γ t else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds L)

Master crossing limit theorem: the PV integral of (γ-s)⁻¹ · γ' along a curve with unique crossing at t₀ tends to L, provided:

1. For small ε, the curve is ε-far from s except near t₀
2. The far-segment integrals sum to some expression E(ε)
3. E(ε) → L as ε → 0⁺

The expression E(ε) is typically log(g(t₀-δ)) - log(g(t₀+δ)) (simple case) or log(g(t₀-δ)) - log(g(t₀+δ)) + correction (when the curve crosses a branch cut of complex log, e.g., the -2πi correction at the elliptic point i).

This is the general version of the pattern used in all 6 ValenceFormula winding number computations.

theorem ContourIntegral.pv_tendsto_of_crossing_limit_asymmetric {γ : ℝ → ℂ} {a b : ℝ} {s L : ℂ} {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioo a b) {δ_left δ_right : ℝ → ℝ} {threshold : ℝ} (hthresh : 0 < threshold) (hδL_pos : ∀ (ε : ℝ), 0 < ε → ε < threshold → 0 < δ_left ε) (hδR_pos : ∀ (ε : ℝ), 0 < ε → ε < threshold → 0 < δ_right ε) (hδL_small : ∀ (ε : ℝ), 0 < ε → ε < threshold → δ_left ε < t₀ - a) (hδR_small : ∀ (ε : ℝ), 0 < ε → ε < threshold → δ_right ε < b - t₀) (h_far_left : ∀ (ε : ℝ), 0 < ε → ε < threshold → ∀ t ∈ Set.Ico a (t₀ - δ_left ε), ε < ‖γ t - s‖) (h_far_right : ∀ (ε : ℝ), 0 < ε → ε < threshold → ∀ t ∈ Set.Ioc (t₀ + δ_right ε) b, ε < ‖γ t - s‖) (h_near : ∀ (ε : ℝ), 0 < ε → ε < threshold → ∀ t ∈ Set.Icc (t₀ - δ_left ε) (t₀ + δ_right ε), ‖γ t - s‖ ≤ ε) {E : ℝ → ℂ} (h_ftc : ∀ (ε : ℝ), 0 < ε → ε < threshold → (∫ (t : ℝ) in a..t₀ - δ_left ε, (γ t - s)⁻¹ * deriv γ t) + ∫ (t : ℝ) in t₀ + δ_right ε..b, (γ t - s)⁻¹ * deriv γ t = E ε) (hint_left : ∀ (ε : ℝ), 0 < ε → ε < threshold → IntervalIntegrable (fun (t : ℝ) => (γ t - s)⁻¹ * deriv γ t) MeasureTheory.volume a (t₀ - δ_left ε)) (hint_right : ∀ (ε : ℝ), 0 < ε → ε < threshold → IntervalIntegrable (fun (t : ℝ) => (γ t - s)⁻¹ * deriv γ t) MeasureTheory.volume (t₀ + δ_right ε) b) (h_limit : Filter.Tendsto E (nhdsWithin 0 (Set.Ioi 0)) (nhds L)) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ‖γ t - s‖ > ε then (γ t - s)⁻¹ * deriv γ t else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds L)

Asymmetric crossing limit: allows different cutoff radii on left and right of the crossing point. Needed for corner crossings (e.g., ρ, ρ+1) where the geometry differs on each side (e.g., vertical segment vs arc).