Per-Term PV Vanishing and CPV Helpers

Per-term PV vanishing for higher-order polar terms (L4), Laurent circle integrals, multi-point CPV, holomorphic CPV vanishing, and assembly helpers.

Main results

• pv_higher_order_term_tendsto_zero: single-crossing higher-order PV → 0
• multipoint_pv_zpow_tendsto_zero: multi-point CPV of zpow → 0
• holomorphic_cpv_tendsto_zero_on_convex: holomorphic CPV → 0 on convex domains
• tendsto_cpv_of_continuousOn_zero_integral: CPV → 0 for continuous functions with zero integral

L4: Per-term PV vanishing for higher-order polar terms

The cutoff integral of a/(γ(t)-s)^{m}·γ'(t) (with m ≥ 2) tends to 0 under the angle condition + flatness, using FTC + boundary vanishing (L3).

The FTC reduces the cutoff integral to boundary terms (γ(t_exit)-s)^{1-m}/(1-m) at the exit points of the ε-ball. These boundary terms are exactly the w^k from L3 with k = 1-m ≤ -1, and flatness of order m gives n + k = m + (1-m) = 1 ≥ 1.

theorem GeneralizedResidueTheory.pv_higher_order_term_tendsto_zero (γ : PiecewiseC1Immersion) (s : ℂ) (m : ℕ) (hm : 2 ≤ m) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = s) (h_unique : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t = s → t = t₀) (hγ_closed : γ.IsClosed) (h_flat : IsFlatOfOrder γ.toFun t₀ m) (h_angle : ∃ (k : ℤ), ↑(m - 1) * angleAtCrossing γ t₀ ht₀ = ↑k * (2 * Real.pi)) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in γ.a..γ.b, if ‖γ.toFun t - s‖ > ε then (γ.toFun t - s) ^ (-↑m) * deriv γ.toFun t else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

For a single crossing at t₀ with angle α, exponent m ≥ 2, and flatness of order m: if (m-1) · α ∈ 2πℤ, then the PV cutoff integral of (γ-s)^{-m} · γ' tends to 0.

This combines FTC telescoping (L1) with boundary vanishing (L3). The flatness hypothesis is essential: without it, the boundary terms (γ-s)^{1-m} at the ε-cutoff points grow as ε^{1-m} → ∞ and the angle condition alone cannot compensate. With flatness of order m, the direction convergence rate is o(ε^{m-1}), which exactly cancels the ε^{1-m} divergence.

theorem GeneralizedResidueTheory.cpvIntegrandOn_sub (S0 : Finset ℂ) (f g : ℂ → ℂ) (γ : ℝ → ℂ) (ε t : ℝ) : cauchyPrincipalValueIntegrandOn S0 f γ ε t - cauchyPrincipalValueIntegrandOn S0 g γ ε t = cauchyPrincipalValueIntegrandOn S0 (fun (z : ℂ) => f z - g z) γ ε t

CPV integrand of f minus CPV integrand of g equals CPV integrand of f - g, pointwise, because both use the same indicator set {t : ∃ s ∈ S0, ‖γ t - s‖ ≤ ε}.

Sublemma 1: Residue equals leading Laurent coefficient

theorem GeneralizedResidueTheory.residueAt_eq_laurent_head_coeff (f : ℂ → ℂ) (s : ℂ) (N : ℕ) (hN : 0 < N) (a : Fin N → ℂ) (g : ℂ → ℂ) (hg : AnalyticAt ℂ g s) (hf_eq : ∀ᶠ (z : ℂ) in nhdsWithin s {s}ᶜ, f z = g z + ∑ k : Fin N, a k / (z - s) ^ (↑k + 1)) : residueAt f s = a ⟨0, hN⟩

Sublemma 1: The residue of f at s equals the leading Laurent coefficient a₀.

Given the Laurent expansion f(z) = g(z) + Σ_{k=0}^{N-1} aₖ/(z-s)^{k+1} near s, with g analytic at s, the circle integral definition of residueAt gives residueAt f s = a₀.

Proof strategy: On a small circle of radius r around s:

• ∮ g = 0 by Cauchy (g analytic → differentiable on disk)
• ∮ (z-s)^{-(k+1)} = 0 for k ≥ 1 (by integral_sub_zpow_of_ne, exponent ≠ -1)
• ∮ (z-s)⁻¹ = 2πi (by integral_sub_center_inv)
• So ∮ f = a₀ · 2πi, hence residueAt f s = (2πi)⁻¹ · a₀ · 2πi = a₀.

theorem GeneralizedResidueTheory.measurableSet_goodSet_Icc (S0 : Finset ℂ) (γ : PiecewiseC1Immersion) (ε : ℝ) : MeasurableSet ({t : ℝ | ∀ s' ∈ S0, ε < ‖γ.toFun t - s'‖} ∩ Set.Icc γ.a γ.b)

Helper 2a: The multi-point "good set" {t | ∀ s' ∈ S0, ε < ‖γ(t)-s'‖} ∩ Icc is measurable.

theorem GeneralizedResidueTheory.aesm_deriv_on_Icc (γ : PiecewiseC1Immersion) : MeasureTheory.AEStronglyMeasurable (deriv γ.toFun) (MeasureTheory.volume.restrict (Set.Icc γ.a γ.b))

The derivative deriv γ.toFun is AEStronglyMeasurable on Icc γ.a γ.b for any PiecewiseC1Immersion γ, because it is continuous off the finite partition set.

theorem GeneralizedResidueTheory.ae_forall_ne_of_finite_crossings (S0 : Finset ℂ) (γ : PiecewiseC1Immersion) : ∀ᵐ (t : ℝ), t ∈ Set.uIoc γ.a γ.b → ∀ s ∈ S0, γ.toFun t ≠ s

A.e. t in the integration interval Ι γ.a γ.b does not land on any point of S0 under γ, because each crossing set is finite (hence null).

Sublemma 2: Multi-point CPV of higher-order pole term → 0

theorem GeneralizedResidueTheory.multipoint_pv_zpow_tendsto_zero (S0 : Finset ℂ) (γ : PiecewiseC1Immersion) (s : ℂ) (m : ℕ) (hm : 2 ≤ m) (hs : s ∈ S0) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = s) (h_unique : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t = s → t = t₀) (hγ_closed : γ.IsClosed) (h_flat : IsFlatOfOrder γ.toFun t₀ m) (h_angle : ∃ (k : ℤ), ↑(m - 1) * angleAtCrossing γ t₀ ht₀ = ↑k * (2 * Real.pi)) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in γ.a..γ.b, cauchyPrincipalValueIntegrandOn S0 (fun (z : ℂ) => (z - s) ^ (-↑m)) γ.toFun ε t) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Sublemma 2: The multi-point CPV integral of (z-s)^{-m} tends to 0 for m ≥ 2, given flatness of order m and the angle condition.

This extends pv_higher_order_term_tendsto_zero from single-point to multi-point cutoff. The difference between multi-point and single-point cutoffs is supported on a set where (z-s)^{-m} is bounded (far from s, near some other s' ∈ S0) and whose measure tends to 0.