Bank jump equals the concrete residue balance

Proved

WeightedRootIntegralIdentity.weightedRootJumpEqualsConcreteResidue

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

complex-analysisjump-integralkeyhole-contourresidue

If the upper and lower banks converge with the orientation-correct conjugacy relation, and the same finite bank sum converges by the concrete Cauchy/residue balance to R, then the real-axis jump A minus its conjugate equals R.

Formal statement

import Mathlib
open Filter Topology
namespace WeightedRootIntegralIdentity
theorem weightedRootJumpEqualsConcreteResidue
    (U L : ℕ → ℂ) (A R : ℂ)
    (hU : Tendsto U atTop (𝓝 A))
    (hL : Tendsto L atTop (𝓝 (-starRingEnd ℂ A)))
    (hres : Tendsto (fun m : ℕ => U m + L m) atTop (𝓝 R)) :
    A - starRingEnd ℂ A = R := by sorry
end WeightedRootIntegralIdentity

Source

Uniqueness of limits applied to the oriented bank-sum sequence, combining the accepted jump-limit and concrete residue theorems.

View graph