have VertIntTendsto : Tendsto (VerticalIntegral (f x)) atTop (𝓝 0) :=
  tendsto_zero_iff_norm_tendsto_zero.mpr AbsVertIntTendsto
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
VertIntBound : ∃ C > 0, ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral (f x)) atTop (𝓝 0)
⊢ VerticalIntegral (f x) σ = 0
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
VertIntBound : ∃ C > 0, ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral (f x)) atTop (𝓝 0)
VertIntTendsto : Tendsto (VerticalIntegral (f x)) atTop (𝓝 0)
⊢ VerticalIntegral (f x) σ = 0