Prove2Me

Finite keyhole limit assembly

Proved
WeightedRootIntegralIdentity.finiteKeyholeLimitAssembly

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

complex-analysiskeyhole-contourlimit-passage

The bank jump follows from the upper and lower boundary limits together with convergence of the finite contour bank sums to the residue value.

Formal statement
import Mathlib
import Theorems.Thm_WeightedRootIntegralIdentity_weightedRootJumpEqualsConcreteResidue
open Filter Topology

theorem WeightedRootIntegralIdentity.finiteKeyholeLimitAssembly
    (U L : ℕ → ℂ) (A ρ : ℂ)
    (hU : Tendsto U atTop (𝓝 A))
    (hL : Tendsto L atTop (𝓝 (-starRingEnd ℂ A)))
    (hres : Tendsto (fun m : ℕ => U m + L m) atTop (𝓝 ρ)) :
    A - starRingEnd ℂ A = ρ := by sorry

View graph