Canonical sequence limits and bank phase

Proved

WeightedRootIntegralIdentity.canonicalSequenceLimitsAndBankPhase

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

branch-limitscomplex-analysiskeyhole-contour

For epsilon_m=1/(m+1) and H_m=m+1, the vertical and arc components vanish in the limit, while the upper/lower branch difference has the phase factor 2i sin(theta).

Formal statement

import Mathlib
open Filter Topology

theorem WeightedRootIntegralIdentity.canonicalSequenceLimitsAndBankPhase
    (VR VL I O : ℕ → ℂ) (upper lower M : ℂ) (theta : ℝ)
    (hVR : Tendsto VR atTop (𝓝 0))
    (hVL : Tendsto VL atTop (𝓝 0))
    (hI : Tendsto I atTop (𝓝 0))
    (hO : Tendsto O atTop (𝓝 0))
    (hphase : upper - lower = 2 * Complex.I * (Real.sin theta : ℂ) * M) :
    Tendsto VR atTop (𝓝 0) ∧ Tendsto VL atTop (𝓝 0) ∧
      Tendsto I atTop (𝓝 0) ∧ Tendsto O atTop (𝓝 0) ∧
      upper - lower = 2 * Complex.I * (Real.sin theta : ℂ) * M := by sorry

View graph