Vanishing of finite vertical contour sides
ProvedWeightedRootIntegralIdentity.vertical_side_vanishasymptoticscomplex-analysiscontour-limit
If the norm of a finite vertical contour contribution is nonnegative and is eventually bounded by a majorant tending to zero as the offset ε decreases to zero, then the vertical contribution vanishes in the one-sided limit.
Preamble
import Mathlib
Formal statement
namespace WeightedRootIntegralIdentity theorem vertical_side_vanish (f M : ℝ → ℝ) (hnonneg : ∀ᶠ ε in nhdsWithin 0 (Set.Ioi 0), 0 ≤ f ε) (hbound : ∀ᶠ ε in nhdsWithin 0 (Set.Ioi 0), f ε ≤ M ε) (hM : Filter.Tendsto M (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) : Filter.Tendsto f (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) := by sorry end WeightedRootIntegralIdentity
Source
One-sided squeeze estimate for finite vertical contour segments.