23.5. ResidueTheorem.PairFormResidueTheorem🔗

Jacobians.ResidueTheorem.PairFormResidueTheorem — source

pairFormResidue

The residue of the meromorphic pair-form h·dg₀ at a, computed in the canonical chart: the resAt of (h ∘ chart⁻¹)·(g₀ ∘ chart⁻¹)′ at the chart image of a (Miranda Ch. VI p. 186: residues of f·dg are chart-independent, so the canonical chart pins the value).

noncomputable def pairFormResidue (g₀ h : MeromorphicFunction X) (a : X) : ℂ

pairFormResidue_eq_zero_of_analyticAt

Res(holo) = 0 for pair-forms: if the pair integrand is analytic at the chart centre (no pole of h·dg₀ at a), the residue vanishes.

theorem pairFormResidue_eq_zero_of_analyticAt (g₀ h : MeromorphicFunction X) (a : X)
    (ha : AnalyticAt ℂ (fun z => h.toFun ((chartAt (H := ℂ) a).symm z)
      * deriv (fun w => g₀.toFun ((chartAt (H := ℂ) a).symm w)) z) ((chartAt (H := ℂ) a) a)) :
    pairFormResidue g₀ h a = 0

pairFormResidue_eq_formFnResidue

The local identity Res_a(h·dg₀) = Res_a((h·q)·ω₀) for q = dg₀/ω₀ — at EVERY point a (no exceptional set!): near the chart centre (off it), q's pullback is the single-chart quotient (derivQuotient_eventuallyEq_chart) and coeffAt ω₀ a ≠ 0 (isolated zeros, ω₀ ≠ 0), so the coeffAt factor cancels and the two resAt integrands agree as germs (resAt_congr).

theorem pairFormResidue_eq_formFnResidue [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] (ω₀ : HolomorphicOneForms X) (hω₀ : ω₀ ≠ 0)
    (g₀ h : MeromorphicFunction X) (a : X) :
    pairFormResidue g₀ h a = formFnResidue ω₀ ((h * derivQuotientFn ω₀ g₀).toFun) a