Abstract

In complex analysis, one often has to manipulate paths, i.e. curves in the complex plane. This entry defines three useful relations on paths:

• an equivalence relation that describes that two paths are the same up to reparametrisation


• a preorder that expresses the notion that one path is a subpath of another


• an equivalence relation that describes equivalence of closed paths up to reparametrisation and "shifting" (e.g. if we have a rectangular path, it does not matter which corner we start in)

• proving each of these relations


• proving well-definedness of paths (path, valid_path)


• determining the image of a path (path_image)


• showing that a path is not self-intersecting (arc, simple_path)


• decomposing integrals on a composite path into the integrals on the constituent paths

BibTeX

@article{Path_Automation-AFP,
  author  = {Manuel Eberl},
  title   = {Path Equivalence and Automation for Integration Contours},
  journal = {Archive of Formal Proofs},
  month   = {October},
  year    = {2025},
  note    = {\url{https://isa-afp.org/entries/Path_Automation.html},
             Formal proof development},
  ISSN    = {2150-914x},
}