Finite keyhole residue limit with vanishing auxiliary terms

Proved

WeightedRootIntegralIdentity.finiteKeyholeResidueLimit

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

complex-analysiscontour-limitresidue-theorem

If the full finite contour sums converge to the residue value and the vertical sides and circular arcs vanish, then the bank sum converges to the same residue value.

Formal statement

import Mathlib
open Filter Topology

theorem WeightedRootIntegralIdentity.finiteKeyholeResidueLimit
    (U L VR VL I O : ℕ → ℂ) (R : ℂ)
    (hfull : Tendsto (fun m : ℕ => U m + L m + VR m + VL m + I m + O m) atTop (𝓝 R))
    (hVR : Tendsto VR atTop (𝓝 0))
    (hVL : Tendsto VL atTop (𝓝 0))
    (hI : Tendsto I atTop (𝓝 0))
    (hO : Tendsto O atTop (𝓝 0)) :
    Tendsto (fun m : ℕ => U m + L m) atTop (𝓝 R) := by sorry

View graph