Upper and lower bank limits give the oriented real-axis jump

Proved

WeightedRootIntegralIdentity.weightedRootUpperLowerLimitOrientedJump

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

complex-analysisconjugationkeyhole-contourlimit-passage

If the upper bank integrals converge to A and the oppositely oriented lower bank integrals converge to the negative conjugate of A, then their sum converges to A minus its conjugate. This is the orientation-correct real-axis jump passage supplied by the upper/lower DCT and conjugacy lemmas.

Formal statement

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

Source

Combine the accepted upper-bank DCT identification, lower-bank conjugacy, and orientation reversal by continuity of addition.

View graph