Concrete finite-to-limiting residue balance for four contour contributions

Proved

WeightedRootIntegralIdentity.concrete_finite_to_limiting_residue_balance

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

complex-analysiscontour-limitkeyhole-contourresidue-theorem

If the four finite truncation contributions converge respectively to the upper-bank, lower-bank, inner-arc, and outer-arc limits, and every finite contour satisfies the residue equation, then the limiting four-term boundary equation holds.

Preamble

import Mathlib
open Filter Topology

Formal statement

namespace WeightedRootIntegralIdentity

theorem concrete_finite_to_limiting_residue_balance (Iu Il Ii Io : ℕ → ℂ) (U L A B residue : ℂ)
    (hu : Filter.Tendsto Iu Filter.atTop (nhds U))
    (hl : Filter.Tendsto Il Filter.atTop (nhds L))
    (hi : Filter.Tendsto Ii Filter.atTop (nhds A))
    (ho : Filter.Tendsto Io Filter.atTop (nhds B))
    (hfinite : ∀ m : ℕ, Iu m + Il m + Ii m + Io m = 2 * Real.pi * Complex.I * residue) :
    U + L + A + B = 2 * Real.pi * Complex.I * residue := by sorry

end WeightedRootIntegralIdentity

Source

Continuity and uniqueness of limits for addition in a Hausdorff topological vector space.

View graph