Apply the accepted contour limit lemmas

Proved

WeightedRootIntegralIdentity.weightedRootApplyAcceptedLimitLemmas

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

complex-analysiskeyhole-contourlimit-passage

Suppose the finite contour equation has constant right-hand side residue. If the upper and lower banks converge to U and L, while the right and left vertical sides and inner and outer arcs vanish, then the limiting bank balance is U+L=residue.

Formal statement

import Mathlib
open Filter Topology
namespace WeightedRootIntegralIdentity
theorem weightedRootApplyAcceptedLimitLemmas
    (Iu Il Vr Vl Ii Io : ℕ → ℂ) (U L residue : ℂ)
    (hu : Tendsto Iu atTop (𝓝 U))
    (hl : Tendsto Il atTop (𝓝 L))
    (hvr : Tendsto Vr atTop (𝓝 0))
    (hvl : Tendsto Vl atTop (𝓝 0))
    (hi : Tendsto Ii atTop (𝓝 0))
    (ho : Tendsto Io atTop (𝓝 0))
    (hfinite : ∀ m : ℕ,
      Iu m + Il m + Vr m + Vl m + Ii m + Io m = residue) :
    U + L = residue := by sorry
end WeightedRootIntegralIdentity

Source

Termwise convergence of the finite contour equation, using the accepted vertical-side, bank, arc, and finite-to-limiting lemmas.

View graph