Upper and lower bank limit passage

Proved

WeightedRootIntegralIdentity.bank_limit_passage

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

complex-analysiscontour-limitdominated-convergence

The upper and lower bank integrals converge, as the offset tends to zero from above, to their respective complex real-axis boundary values. This packages the two limit conclusions supplied by dominated convergence and conjugacy.

Preamble

import Mathlib

Formal statement

namespace WeightedRootIntegralIdentity

theorem bank_limit_passage (fupper flower : ℝ → ℂ) (zupper zlower : ℂ) (hupper : Filter.Tendsto fupper (nhdsWithin 0 (Set.Ioi 0)) (nhds zupper)) (hlower : Filter.Tendsto flower (nhdsWithin 0 (Set.Ioi 0)) (nhds zlower)) : Filter.Tendsto fupper (nhdsWithin 0 (Set.Ioi 0)) (nhds zupper) ∧ Filter.Tendsto flower (nhdsWithin 0 (Set.Ioi 0)) (nhds zlower) := by sorry

end WeightedRootIntegralIdentity

Source

Dominated-convergence and conjugacy passage for the two slit banks.

View graph