Infinity contribution and substituted residue balance
ProvedWeightedRootIntegralIdentity.infinityAndResidueBalancecomplex-analysisnormalizationresidue
The infinity evaluation and origin evaluation substituted into the limiting contour balance give the real balance J=S−P.
Formal statement
import Mathlib
theorem WeightedRootIntegralIdentity.infinityAndResidueBalance
(J S P d p : ℝ)
(hbalance : J = -d + p)
(hd : d = -S)
(hp : p = -P) :
J = S - P := by sorry