A machine-checked solution to the Jacobians challenge

23. residue theorem🔗

The unconditional residue theorem ∑_p Res_p(h·dg₀) = 0 for meromorphic pair forms on a compact surface, any genus, via partition of unity + planar Stokes.

8 modules, 2,310 lines, under Jacobians/ResidueTheorem/.

References: Miranda Ch. VI pp. 186–188 · Miranda Ch. VI p. 186 · Forster GTM 81 §10 · Forster GTM 81, Theorem 10.21.

  1. 23.1. Keystones
  2. 23.2. Builds on
  3. 23.3. ResidueTheorem
  4. 23.4. ResidueTheorem.OmegaFactorization
  5. 23.5. ResidueTheorem.PairFormResidueTheorem
  6. 23.6. ResidueTheorem.ResidueLedgerTransport
  7. 23.7. ResidueTheorem.ResidueStokesCoverPoU
  8. 23.8. ResidueTheorem.ResidueStokesPoleBump
  9. 23.9. ResidueTheorem.ResidueTheoremFormFn
  10. 23.10. ResidueTheorem.ResidueTheoremStokes