Identify the bank jump with the concrete residue

import Mathlib
import Theorems.Thm_WeightedRootIntegralIdentity_weightedRootUpperLowerLimitOrientedJump
import Theorems.Thm_WeightedRootIntegralIdentity_weightedRootJumpEqualsConcreteResidue
open Filter Topology

theorem WeightedRootIntegralIdentity.weightedRootIdentifyJumpAndResidue
    (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ρ