Finite-to-limiting contour equation

Proved

WeightedRootIntegralIdentity.finite_to_limiting_contour_equation

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

complex-analysiscontour-limitkeyhole-contour

After passing to the contour limits, the upper and lower bank contributions converge to limiting values U and L, while the inner and outer contributions vanish. If the limiting rectangle equation is U + L = 2πi times the residue, then the full limiting boundary equation follows.

Preamble

import Mathlib

Formal statement

namespace WeightedRootIntegralIdentity

theorem finite_to_limiting_contour_equation (Iupper Ilower Iinner Iouter U L residue : ℂ) (hupper : Iupper = U) (hlower : Ilower = L) (hinner : Iinner = 0) (houter : Iouter = 0) (hrect : U + L = 2 * Real.pi * Complex.I * residue) : Iupper + Ilower + Iinner + Iouter = 2 * Real.pi * Complex.I * residue := by sorry

end WeightedRootIntegralIdentity

Source

Finite-to-limiting passage for the weighted-root keyhole contour.

View graph