23.9. ResidueTheorem.ResidueTheoremFormFn🔗

Jacobians.ResidueTheorem.ResidueTheoremFormFn — source

derivQuotientFn_orderW_ne_top

KEY LEMMA: the quotient q = dg₀/ω₀ of a nonconstant g₀ by a nonzero ω₀ is nowhere germ-zero (orderW ≠ ⊤ at every point). If the chart read of q were eventually 0 near some a, then — since q's read agrees off the centre with (g₀∘chart⁻¹)′ / coeffAt ω₀ a (derivQuotient_eventuallyEq_chart) and coeffAt ω₀ a is eventually nonzero (isolated zeros, ω₀ ≠ 0) — the derivative (g₀∘chart⁻¹)′ would vanish on a punctured neighbourhood, i.e. formOrderW (dg₀) a = ⊤; the form identity theorem (MeromorphicOneForm.formOrderW_ne_top_of_exists) then contradicts dg₀ ≠ 0 (differentialForm_ne_zero, from ¬ IsGermConstant g₀).

theorem derivQuotientFn_orderW_ne_top (ω₀ : HolomorphicOneForms X) (hω₀ : ω₀ ≠ 0)
    {g₀ : MeromorphicFunction X} (hg₀ : ¬ IsGermConstant g₀) (a : X) :
    (derivQuotientFn ω₀ g₀).orderW a ≠ ⊤

residueTheorem_formFn_unconditional

THE 1-FORM RESIDUE THEOREM, ALL GENERA (Forster GTM 81, 10.21): for a global holomorphic 1-form ω₀ and a meromorphic g on the compact Riemann surface X, the total residue over any finite set containing the poles vanishes,

∑ a ∈ poles, formFnResidue ω₀ g.toFun a = 0,

provided g's chart read is honestly AnalyticAt at every chart centre off poles. NO genus hypothesis: reduction to the planar-Stokes pair-form theorem residueSum_pairForm_eq_zero_unconditional via the reverse ω₀-factorization ω₀·g = h·dg₀, h := g·(dg₀/ω₀)⁻¹, for a nonconstant g₀ (derivQuotientFn_orderW_ne_top supplies the eventual nonvanishing that repairs the germ g·q⁻¹·q = g).

theorem residueTheorem_formFn_unconditional [Nonempty X]
    (ω₀ : HolomorphicOneForms X) (g : MeromorphicFunction X) (poles : Finset X)
    (hpoles : ∀ x : X, x ∉ poles →
      AnalyticAt ℂ (fun z => g.toFun ((chartAt ℂ x).symm z)) ((chartAt ℂ x) x)) :
    ∑ a ∈ poles, formFnResidue ω₀ g.toFun a = 0