23.1. Keystones🔗

residueSum_pairForm_eq_zero_unconditional — source · report an issue

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