Remote contour bound tends to zero
ProvedWeightedRootIntegralIdentity.remote_boundary_norm_vanishasymptoticscomplex-analysiscontour-limit
If a nonnegative remote-contour norm is eventually bounded above by a majorant that tends to zero as the radius tends to infinity, then the contour norm itself tends to zero. This is the squeeze step used to discard remote boundary pieces in the keyhole limit.
Preamble
import Mathlib
Formal statement
namespace WeightedRootIntegralIdentity theorem remote_boundary_norm_vanish (f M : ℝ → ℝ) (hnonneg : ∀ᶠ R in Filter.atTop, 0 ≤ f R) (hbound : ∀ᶠ R in Filter.atTop, f R ≤ M R) (hM : Filter.Tendsto M Filter.atTop (nhds 0)) : Filter.Tendsto f Filter.atTop (nhds 0) := by sorry end WeightedRootIntegralIdentity
Source
Squeeze estimate for remote contour contributions.