Upper and lower bank boundary-limit passage
ProvedWeightedRootIntegralIdentity.bankBoundaryLimitPassageboundary-limitscomplex-analysiskeyhole-contour
If the upper and lower finite-bank integrals converge as epsilon approaches zero from above, their oriented sum converges to the sum of the two boundary values.
Formal statement
import Mathlib
open Filter Topology
theorem WeightedRootIntegralIdentity.bankBoundaryLimitPassage
(U L : ℝ → ℂ) (A B : ℂ)
(hU : Tendsto U (𝓝[>] (0 : ℝ)) (𝓝 A))
(hL : Tendsto L (𝓝[>] (0 : ℝ)) (𝓝 B)) :
Tendsto (fun ε : ℝ => U ε + L ε) (𝓝[>] (0 : ℝ)) (𝓝 (A + B)) := by sorry