The residue sum along the boundary contour

The Hungerbühler–Wasem residue sum, instantiated on the boundary contour of the truncated fundamental domain: for a function with a polar-part decomposition whose poles all lie in the open truncated domain, the principal value of the contour integral is -2πi times the sum of the residues — the contour winds -1 about every interior point, and the corner conditions of the general theorem hold vacuously because the contour avoids the poles.

This is the contour side of the valence formula: applied to the logarithmic derivative of a modular form, the residues become the orders of its zeros.

Main declarations

• TauCeti.ModularForm.hasCauchyPV_fdBoundary_residue_sum.

References

The truncated-contour strategy follows the fundamental-domain boundary development of AINTLIB's LeanModularForms (ForMathlib/FDBoundary.lean, FDBoundaryH.lean, FDBoundaryPath.lean); the residue machinery is Tau Ceti's Hungerbühler–Wasem development.

theorem TauCeti.ModularForm.hasCauchyPV_fdBoundary_residue_sum {H : ℝ} (hH : 1 < H) {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} (decomp : Contour.PolarPartDecomposition f S U) (hU : IsOpen U) (hUdom : UpperHalfPlane.coe '' ModularGroup.truncatedFundamentalDomain H ⊆ U) (hS : ∀ s ∈ S, 1 < ‖s‖ ∧ |s.re| < 1 / 2 ∧ 0 < s.im ∧ s.im < H) : Contour.HasCauchyPV (fdBoundary H) 0 5 f (-(2 * ↑Real.pi * Complex.I) * ∑ s ∈ S, Contour.residue f s)

The residue sum along the boundary contour. For a function with a polar-part decomposition on an open set containing the closed truncated fundamental domain, all of whose poles lie in the open truncated domain, the principal value of the contour integral is -2πi times the sum of the residues: the contour winds -1 about every pole.