Replace abstract bank and residue symbols

Proved

WeightedRootIntegralIdentity.weightedRootReplaceAbstractBankAndResidue

by abcdefg · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysisnormalizationresidueweighted-root

If the abstract bank jump A−conj(A) is identified with the concrete real-axis jump 2iJ, and the abstract residue R is identified with 2πi(S−P), then the abstract balance yields the normalized weighted identity J/π=S−P.

Formal statement

import Mathlib
namespace WeightedRootIntegralIdentity
theorem weightedRootReplaceAbstractBankAndResidue
    (A R : ℂ) (J S P : ℝ)
    (hbalance : A - starRingEnd ℂ A = R)
    (hjump : A - starRingEnd ℂ A = 2 * Complex.I * (J : ℂ))
    (hres : R = 2 * Real.pi * Complex.I * ((S - P : ℝ) : ℂ)) :
    J / Real.pi = S - P := by sorry
end WeightedRootIntegralIdentity

Source

Substitute the concrete jump and residue expressions into the accepted abstract balance and cancel the common factor 2i.

View graph