23.10. ResidueTheorem.ResidueTheoremStokes🔗

Jacobians.ResidueTheorem.ResidueTheoremStokes — source

ledgerIntegrand_sum_P

Scalar-field sums pass through the ledger integrand (the field enters by value).

theorem ledgerIntegrand_sum_P {ι : Type*} (s : Finset ι) (PF : ι → X → ℂ)
    (g₀ h : MeromorphicFunction X) (v : X → ℝ) (y : X) (V : Set X) (z : ℂ) :
    ∑ i ∈ s, ledgerIntegrand g₀ h (PF i) v y V z
      = ledgerIntegrand g₀ h (fun x => ∑ i ∈ s, PF i x) v y V z

ledgerIntegrand_const_v

A constant cutoff has vanishing ∂̄-read: the ledger integrand is identically 0.

theorem ledgerIntegrand_const_v (g₀ h : MeromorphicFunction X) (P : X → ℂ) (cst : ℝ)
    (y : X) (V : Set X) : ledgerIntegrand g₀ h P (fun _ => cst) y V = fun _ => 0

meromorphicAt_pairRead

The pair coefficient is meromorphic at its own chart centre.

theorem meromorphicAt_pairRead (g₀ h : MeromorphicFunction X) (a : X) :
    MeromorphicAt (pairRead g₀ h a) ((chartAt (H := ℂ) a) a)

PoleBumpData.dbar_bumpRead

The ∂̄-read of the pole bump in its own chart is the explicit radial closed form η′(normSq(z−c))·(z−c).

theorem PoleBumpData.dbar_bumpRead {S : Finset X} (D : PoleBumpData S) {a : X} (ha : a ∈ S)
    {z : ℂ} (hz : z ∈ (chartAt (H := ℂ) a).target) :
    DbarDisk.dbar (fun w => ((D.bump a ((chartAt (H := ℂ) a).symm w) : ℝ) : ℂ)) z
      = Complex.ofReal (deriv (D.η a) (Complex.normSq (z - (chartAt (H := ℂ) a) a)))
        * (z - (chartAt (H := ℂ) a) a)

uC

The complexified total bump.

noncomputable def uC (D : PoleBumpData S) : X → ℂ

continuous_uC

theorem continuous_uC [CompactSpace X] [T2Space X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] : Continuous (uC D)

readsAnalyticAt_of_notMem

Good points off S.

theorem readsAnalyticAt_of_notMem (hSbad : ∀ x : X, ¬ ReadsAnalyticAt g₀ h x → x ∈ S)
    (x : X) (hx : x ∉ (S : Set X)) :
    ReadsAnalyticAt g₀ h x

integral_psi_eq

(L1) ∫_ℂ η′_a(normSq(z−c_a))·(z−c_a)·f_a(z) = −π·pairFormResidue g₀ h a — the closed-form single-pole atom, applied to the pair coefficient in the chart at a.

theorem integral_psi_eq [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (hSbad : ∀ x : X, ¬ ReadsAnalyticAt g₀ h x → x ∈ S)
    {a : X} (ha : a ∈ S) :
    ∫ z : ℂ, (Complex.ofReal (deriv (D.η a)
        (Complex.normSq (z - (chartAt (H := ℂ) a) a)))
      * (z - (chartAt (H := ℂ) a) a) * pairRead g₀ h a z)
      = -(π : ℂ) * pairFormResidue g₀ h a

poleWindow

The window of the (a,j) ledger piece: the pole chart's source meets the PoU chart.

def poleWindow [T2Space X] [CompactSpace X] (a : X)
    (j : Fin ((chartCover : Finset X).card)) : Set X

poleWindow_isOpen

theorem poleWindow_isOpen [T2Space X] [CompactSpace X] (a : X)
    (j : Fin ((chartCover : Finset X).card)) :
    IsOpen (poleWindow (X := X) a j)

poleWindow_subset_pole

theorem poleWindow_subset_pole [T2Space X] [CompactSpace X] (a : X)
    (j : Fin ((chartCover : Finset X).card)) :
    poleWindow (X := X) a j ⊆ (chartAt (H := ℂ) a).source

poleWindow_subset_cover

theorem poleWindow_subset_cover [T2Space X] [CompactSpace X] (a : X)
    (j : Fin ((chartCover : Finset X).card)) :
    poleWindow (X := X) a j ⊆ (chartAt (H := ℂ) (coverCenter j)).source

rho_psi_eq_ledger

(L2 bridge) the raw ρ_j-weighted pole integrand IS the (a,j) ledger integrand:

ρ_j(chart_a⁻¹ z)·[η′_a·(z−c_a)·f_a(z)] = ledgerIntegrand (ρC_j) (bump a) a (poleWindow a j).

Off the window everything vanishes pointwise (the profile derivative below ε²/4/above ε²/2; the PoU factor off tsupport ρ_j on the annulus).

theorem rho_psi_eq_ledger [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] {a : X} (ha : a ∈ S) (j : Fin ((chartCover : Finset X).card)) :
    (fun z : ℂ => coverRhoC (X := X) j ((chartAt (H := ℂ) a).symm z)
        * (Complex.ofReal (deriv (D.η a) (Complex.normSq (z - (chartAt (H := ℂ) a) a)))
          * (z - (chartAt (H := ℂ) a) a) * pairRead g₀ h a z))
      = ledgerIntegrand g₀ h (coverRhoC (X := X) j) (D.bump a) a (poleWindow a j)

bump_locally_const_on_S

Every pole bump is locally constant near every point of S (1 near its own pole, 0 near the others).

theorem bump_locally_const_on_S [T2Space X] {a : X} (ha : a ∈ S) {p : X} (hp : p ∈ S) :
    ∃ cst : ℝ, ∀ᶠ x' in 𝓝 p, D.bump a x' = cst

totalBump_locally_const_on_S

The total bump is locally ≡ 1 near every point of S.

theorem totalBump_locally_const_on_S [T2Space X] {p : X} (hp : p ∈ S) :
    ∃ cst : ℝ, ∀ᶠ x' in 𝓝 p, D.totalBump x' = cst

uC_sub_one_eventually_zero

uC − 1 vanishes locally near every point of S.

theorem uC_sub_one_eventually_zero [T2Space X]
    (_hSbad : ∀ x : X, ¬ ReadsAnalyticAt g₀ h x → x ∈ S)
    {p : X} (hp : p ∈ S) : ∀ᶠ x' in 𝓝 p, uC D x' - 1 = 0

integrable_polePiece

Integrability of the (a,j) pole pieces (in either chart, over any window containing the compact core poleBall a ∩ tsupport ρ_j).

theorem integrable_polePiece [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (hSbad : ∀ x : X, ¬ ReadsAnalyticAt g₀ h x → x ∈ S)
    {a : X} (ha : a ∈ S) (j : Fin ((chartCover : Finset X).card))
    {y : X} {V : Set X} (hVopen : IsOpen V) (hVsub : V ⊆ (chartAt (H := ℂ) y).source)
    (hKV : D.poleBall a ∩ tsupport (coverPoU (X := X) j) ⊆ V) :
    Integrable (ledgerIntegrand g₀ h (coverRhoC (X := X) j) (D.bump a) y V) volume

integrable_dRhoPiece

Integrability of ∂̄ρ_j-pieces: scalar field P vanishing near every point of S, cutoff ρ_j, any window with a compact core outside which P vanishes or ρ_j does.

theorem integrable_dRhoPiece [T2Space X] [CompactSpace X] [IsManifold 𝓘(ℂ) ω X]
    (hSbad : ∀ x : X, ¬ ReadsAnalyticAt g₀ h x → x ∈ S)
    {P : X → ℂ} (hP : Continuous P) (hPkill : ∀ p ∈ S, ∀ᶠ x' in 𝓝 p, P x' = 0)
    (j : Fin ((chartCover : Finset X).card))
    {y : X} {V : Set X} (hVopen : IsOpen V) (hVsub : V ⊆ (chartAt (H := ℂ) y).source)
    {K : Set X} (hK : IsCompact K) (hKV : K ⊆ V)
    (hkill : ∀ x ∈ V, x ∉ K → P x = 0 ∨ x ∉ tsupport (coverPoU (X := X) j)) :
    Integrable (ledgerIntegrand g₀ h P (fun x => coverPoU (X := X) j x) y V) volume

integrable_B

Integrability of the B_j aggregate (PoU scalar, total-bump cutoff).

theorem integrable_B [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (hSbad : ∀ x : X, ¬ ReadsAnalyticAt g₀ h x → x ∈ S)
    (j : Fin ((chartCover : Finset X).card)) :
    Integrable (ledgerIntegrand g₀ h (coverRhoC (X := X) j) D.totalBump
      (coverCenter j) (chartOpen (X := X) (coverCenter j))) volume

integral_A_add_integral_B

(L5) Per PoU chart j, planar Stokes for Φ = ρ̂_j·(û−1)·f̂_j (which is C¹ with compact support: û ≡ 1 near the poles kills the singularities of f̂) gives, via Leibniz,

∫_ℂ (û−1)·∂̄ρ̂_j·f̂_j + ∫_ℂ ρ̂_j·∂̄û·f̂_j = 0.

theorem integral_A_add_integral_B [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (hSbad : ∀ x : X, ¬ ReadsAnalyticAt g₀ h x → x ∈ S)
    (j : Fin ((chartCover : Finset X).card)) :
    (∫ w, ledgerIntegrand g₀ h (fun x => uC D x - 1) (fun x => coverPoU (X := X) j x)
        (coverCenter j) (chartOpen (X := X) (coverCenter j)) w)
      + (∫ w, ledgerIntegrand g₀ h (coverRhoC (X := X) j) D.totalBump
        (coverCenter j) (chartOpen (X := X) (coverCenter j)) w) = 0

integral_Xi_transport

The (j,i) transported piece: shrink to the chart overlap (the ρ_i factor vanishes off chartOpen c_i), transport c_j → c_i, enlarge (the ρ_j cutoff dies off chartOpen c_j).

theorem integral_Xi_transport [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (hSbad : ∀ x : X, ¬ ReadsAnalyticAt g₀ h x → x ∈ S)
    (j i : Fin ((chartCover : Finset X).card)) :
    (∫ w, ledgerIntegrand g₀ h (fun x => coverRhoC (X := X) i x * (uC D x - 1))
        (fun x => coverPoU (X := X) j x)
        (coverCenter j) (chartOpen (X := X) (coverCenter j)) w)
      = ∫ w, ledgerIntegrand g₀ h (fun x => coverRhoC (X := X) i x * (uC D x - 1))
          (fun x => coverPoU (X := X) j x)
          (coverCenter i) (chartOpen (X := X) (coverCenter i)) w

sum_integral_A_eq_zero

(L6) ∑_j ∫ A_j = 0: insert 1 = ∑_i ρ_i, transport each (j,i) piece to chart i, and let ∑_j ∂̄ρ̂_j = ∂̄(1) = 0 kill each chart-i aggregate.

theorem sum_integral_A_eq_zero [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (hSbad : ∀ x : X, ¬ ReadsAnalyticAt g₀ h x → x ∈ S) :
    ∑ j, (∫ w, ledgerIntegrand g₀ h (fun x => uC D x - 1)
        (fun x => coverPoU (X := X) j x)
        (coverCenter j) (chartOpen (X := X) (coverCenter j)) w) = 0

residueSum_pairForm_eq_zero_S

The residue ledger assembled: over the enlarged pole set S (containing the analytic bad locus), ∑_{a ∈ S} pairFormResidue g₀ h a = 0.

theorem residueSum_pairForm_eq_zero_S [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [Nonempty X] [IsManifold 𝓘(ℂ) ω X]
    (hSbad : ∀ x : X, ¬ ReadsAnalyticAt g₀ h x → x ∈ S) :
    ∑ a ∈ S, pairFormResidue g₀ h a = 0

residueSum_pairForm_eq_zero_unconditional

THE PAIR-FORM RESIDUE THEOREM, ALL GENERA (Forster GTM 81, 10.21): the total residue of a meromorphic pair-form h·dg₀ over any finite set containing its poles vanishes,

∑ a ∈ poles, pairFormResidue g₀ h a = 0,

provided the pair integrand is honestly AnalyticAt at every chart centre off poles. NO genus hypothesis: the planar-Stokes ledger (single-pole annulus atoms + chart transport + partition of unity + Forster 10.20) replaces the ω₀-factorization of the genus ≥ 1 proof.

theorem residueSum_pairForm_eq_zero_unconditional
    (g₀ h : MeromorphicFunction X) (poles : Finset X)
    (hpoles : ∀ x, x ∉ poles → AnalyticAt ℂ
      (fun z => h.toFun ((chartAt (H := ℂ) x).symm z)
         * deriv (fun w => g₀.toFun ((chartAt (H := ℂ) x).symm w)) z)
      ((chartAt (H := ℂ) x) x)) :
    ∑ a ∈ poles, pairFormResidue g₀ h a = 0

residueSum_pairForm_mul_eq_zero_unconditional

Convenience wrapper for product numerators, all genera (the downstream Mittag–Leffler/Serre-pairing shape ∑Res(f·h·dg₀) = 0): the main theorem at the pair (g₀, f·h), with the analyticity hypothesis stated on the unfolded product integrand.

theorem residueSum_pairForm_mul_eq_zero_unconditional
    (g₀ f h : MeromorphicFunction X) (poles : Finset X)
    (hpoles : ∀ x, x ∉ poles → AnalyticAt ℂ
      (fun z => f.toFun ((chartAt (H := ℂ) x).symm z) * h.toFun ((chartAt (H := ℂ) x).symm z)
         * deriv (fun w => g₀.toFun ((chartAt (H := ℂ) x).symm w)) z)
      ((chartAt (H := ℂ) x) x)) :
    ∑ a ∈ poles, pairFormResidue g₀ (f * h) a = 0