Per-Term PV Vanishing: CPV Helpers and Assembly

CPV helpers for continuous functions, holomorphic CPV vanishing on convex domains, scalar/sum lemmas for CPV integrands, integrability, and the assembly of per-term vanishing into the complete higher-order cancellation.

Main Results

• tendsto_cpv_of_continuousOn_zero_integral — CPV with zero contour integral
• holomorphic_cpv_tendsto_zero_on_convex — holomorphic CPV → 0
• cpvIntegrandOn_const_smul / cpvIntegrandOn_add / cpvIntegrandOn_finset_sum
• intervalIntegrable_cpvIntegrandOn_of_continuousOn_diff
• residueAt_sub_residueSum_eq_zero — residue of f minus residue sum vanishes
• cpv_tendsto_zero_of_add_decomposition — final assembly

Helper: CPV of a function continuous along γ with zero contour integral

If g is continuous on γ's image and ∮_γ g dz = 0, then cpv(S0, g, ε) → 0. The CPV integrand converges a.e. to g(γ(t)) * γ'(t) as ε → 0 (the crossing set has measure zero), and is dominated by ‖g(γ(t))‖ * ‖γ'(t)‖. By DCT, the limit equals ∮_γ g dz = 0.

theorem GeneralizedResidueTheory.tendsto_cpv_of_continuousOn_zero_integral (S0 : Finset ℂ) (g : ℂ → ℂ) (γ : PiecewiseC1Immersion) (hg_cont : ContinuousOn g (γ.toFun '' Set.Icc γ.a γ.b)) (h_integral_zero : ∫ (t : ℝ) in γ.a..γ.b, g (γ.toFun t) * deriv γ.toFun t = 0) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in γ.a..γ.b, cauchyPrincipalValueIntegrandOn S0 g γ.toFun ε t) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

CPV integral of a function continuous along γ with zero ordinary contour integral tends to 0. This is the DCT core of the assembly proof, abstracting the zero-integral condition.

Sublemma 3: Holomorphic CPV integral → 0 on closed curve

theorem GeneralizedResidueTheory.holomorphic_cpv_tendsto_zero_on_convex (U : Set ℂ) (hU : IsOpen U) (hU_convex : Convex ℝ U) (S0 : Finset ℂ) (g : ℂ → ℂ) (hg : DifferentiableOn ℂ g U) (γ : PiecewiseC1Immersion) (hγ_closed : γ.IsClosed) (hγ_in_U : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ∈ U) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in γ.a..γ.b, cauchyPrincipalValueIntegrandOn S0 g γ.toFun ε t) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Sublemma 3: For a function holomorphic on a convex open U containing the closed curve γ, the multi-point CPV integral tends to 0.

The CPV integrand 1_{∀s∈S0, ‖γ(t)-s‖>ε} · g(γ(t)) · γ'(t) converges a.e. to g(γ(t)) · γ'(t) as ε → 0 (the cutout set shrinks to a null set), and is dominated by ‖g(γ(t))‖ · ‖γ'(t)‖ (bounded since g is continuous on the compact image of γ). By DCT, the CPV integral converges to the ordinary integral ∮_γ g dz, which is 0 by Cauchy's integral theorem on convex U.

Helper: CPV integral of scalar multiple

theorem GeneralizedResidueTheory.cpvIntegrandOn_const_smul (S0 : Finset ℂ) (c : ℂ) (f : ℂ → ℂ) (γ : ℝ → ℂ) (ε t : ℝ) : cauchyPrincipalValueIntegrandOn S0 (fun (z : ℂ) => c * f z) γ ε t = c * cauchyPrincipalValueIntegrandOn S0 f γ ε t

CPV integrand of c • f equals c • cpv(f) pointwise (the indicator set is the same).

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

CPV integrand of f + g equals cpv(f) + cpv(g) pointwise (same indicator).

theorem GeneralizedResidueTheory.cpvIntegrandOn_finset_sum {ι : Type u_1} (S0 : Finset ℂ) (T : Finset ι) (f : ι → ℂ → ℂ) (γ : ℝ → ℂ) (ε t : ℝ) : cauchyPrincipalValueIntegrandOn S0 (fun (z : ℂ) => ∑ i ∈ T, f i z) γ ε t = ∑ i ∈ T, cauchyPrincipalValueIntegrandOn S0 (f i) γ ε t

CPV integrand of a finset sum decomposes.

theorem GeneralizedResidueTheory.intervalIntegrable_cpvIntegrandOn_of_continuousOn_diff (U : Set ℂ) (S0 : Finset ℂ) (g : ℂ → ℂ) (hg_cont : ContinuousOn g (U \ ↑S0)) (γ : PiecewiseC1Immersion) (hγ_in_U : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ∈ U) (ε : ℝ) (hε : 0 < ε) : IntervalIntegrable (cauchyPrincipalValueIntegrandOn S0 g γ.toFun ε) MeasureTheory.volume γ.a γ.b

Integrability of CPV integrand for functions continuous on U \ S0. For any g continuous on U \ S0 with γ mapping into U, the multi-point CPV integrand is interval integrable on [a,b] for fixed ε > 0. The key insight is that the CPV integrand is bounded (it's either 0 or g(γ(t)) * γ'(t) where γ(t) is far from all poles) and ae strongly measurable (continuous off a finite set within [a,b]).

Assembly helper: CPV of h = f - f_res tends to 0

This helper packages the assembly of Sublemmas 1-3 into the main bridge lemma. It shows that ∫ cpv(S0, h, ε) → 0 where h z = f z - Σ res(f,s)/(z-s).

The proof decomposes h into:

• Polar terms at each crossed point: a_k/(z-s)^{k+1} for k ≥ 1, each tending to 0 by multipoint_pv_zpow_tendsto_zero (Sublemma 2).
• Holomorphic remainder: continuous along γ with zero contour integral, tending to 0 by tendsto_cpv_of_continuousOn_zero_integral.

The identification a_0 = residueAt f s uses residueAt_eq_laurent_head_coeff (Sublemma 1).

theorem GeneralizedResidueTheory.residueAt_sub_residueSum_eq_zero (S0 : Finset ℂ) (f : ℂ → ℂ) (s : ℂ) (hs : s ∈ S0) (hMero : MeromorphicAt f s) : residueAt (fun (z : ℂ) => f z - ∑ s' ∈ S0, residueAt f s' / (z - s')) s = 0

Helper: residueAt (f - Σ res(f,s')/(z-s')) s = 0 for s ∈ S0. The function h z = f z - Σ_{s' ∈ S0} residueAt f s' / (z - s') has the same higher-order poles as f at s but no simple pole (the s' = s term in the sum cancels the residue). Hence residueAt h s = 0.

The proof uses circle integral decomposition: for small r, ∮_{C(s,r)} h = ∮ f - Σ residueAt f s' * ∮ 1/(z-s'). For s' ≠ s with |s'-s| > r, ∮ 1/(z-s') = 0 (Cauchy); for s' = s, ∮ 1/(z-s) = 2πi. So (2πi)⁻¹ ∮ h = (2πi)⁻¹ ∮ f - residueAt f s. Taking r → 0: residueAt h s = residueAt f s - residueAt f s = 0.