Boundary equation from limiting contour components

Proved

WeightedRootIntegralIdentity.contour_boundary_from_limit_components

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

complex-analysiscontour-limitkeyhole-contour

Suppose the limiting upper and lower bank integrals combine into twice a bank contribution, the inner and outer arc limits cancel, and the limiting total boundary integral equals the residue contribution. Then twice the bank contribution equals the residue term. This packages the final passage from contour-component limits to the boundary equation.

Preamble

import Mathlib
import Theorems.Thm_WeightedRootIntegralIdentity_contour_limit_assembly

Formal statement

namespace WeightedRootIntegralIdentity

theorem contour_boundary_from_limit_components (Iupper Ilower Iinner Iouter residue Ibank : ℂ) (hbank : Iupper + Ilower = 2 * Ibank) (harcs : Iinner + Iouter = 0) (hboundary : Iupper + Ilower + Iinner + Iouter = 2 * Real.pi * Complex.I * residue) : 2 * Ibank = 2 * Real.pi * Complex.I * residue := by sorry

end WeightedRootIntegralIdentity

Source

Limit passage for the weighted-root keyhole contour.

View graph