The Detour Calculus: Rigorous Local Deformation of Integration Contours

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 $\gamma$ to a family of deformed contours $(\gamma_\epsilon)_{\epsilon > 0}$
• theorems that allow transferring geometric properties from $\gamma$ to $\gamma_\epsilon$ for sufficiently small $\epsilon$
• 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.