Finite contour decomposition and residue equation
ProvedWeightedRootIntegralIdentity.finiteContourDecompositionResidueEquationcomplex-analysiscontour-integralresidue-theorem
If the assembled finite contour integral decomposes into upper bank, lower bank, vertical sides, and circular arcs, and the residue theorem evaluates the assembled contour, then the six component integrals satisfy the finite residue equation.
Formal statement
import Mathlib
theorem WeightedRootIntegralIdentity.finiteContourDecompositionResidueEquation
(C U L VR VL I O residue : ℂ)
(hdecomp : C = U + L + VR + VL + I + O)
(hres : C = 2 * Real.pi * Complex.I * residue) :
U + L + VR + VL + I + O = 2 * Real.pi * Complex.I * residue := by sorry