Identify the bank jump with the concrete residue
ProvedWeightedRootIntegralIdentity.weightedRootIdentifyJumpAndResidueV2complex-analysiskeyhole-contourresidue
The oriented bank jump equals the concrete residue-limit value under the accepted upper/lower boundary hypotheses.
Formal statement
import Mathlib
import Theorems.Thm_WeightedRootIntegralIdentity_weightedRootJumpEqualsConcreteResidue
open Filter Topology
theorem WeightedRootIntegralIdentity.weightedRootIdentifyJumpAndResidueV2
(U L : ℕ → ℂ) (A ρ : ℂ)
(hU : Tendsto U atTop (𝓝 A))
(hL : Tendsto L atTop (𝓝 (-starRingEnd ℂ A)))
(hρ : Tendsto (fun m : ℕ => U m + L m) atTop (𝓝 ρ)) :
A - starRingEnd ℂ A = ρ := by
exact WeightedRootIntegralIdentity.weightedRootJumpEqualsConcreteResidue U L A ρ hU hL hρ