Email Gateway (Jun 18 2026 at 13:44): Email Gateway (Jun 18 2026 at 13:44):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to welcome yet another contribution from the ever prolific Manuel Eberl!
Larry
The Detour Calculus: Rigorous Local Deformation of Integration Contours
Manuel Eberl
This entry provides the detour calculus, a relational framework to construct deformed versions of integration contours by adding small indentations around problematic points (typically poles). It consists of:
the definition of a relation that relates the original contour to a family of deformed contours
theorems that allow transferring geometric properties from to for sufficiently small
a library of “basic avoidance patterns” to add indentations to lines, circular arcs, or the corners between them, and prove that they are in relation with the original contour
a calculus of inference rules which, in particular, allows dealing with composite contours by proving the relation for its individual parts separately
The motivating example for this calculus was the proof of the valence formula for modular forms (not included here), which requires such a complicated set of indentations that I deemed it beyond the reach of formalisation without a systematic approach such as the present one.
https://isa-afp.org/entries/Detour_Calculus.html
Last updated: Jul 02 2026 at 07:34 UTC