have VertIntBound : ∃ C > 0, ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x^σ' * C := by
  let C := ∫ (t : ℝ), 1 / ((1 + t ^ 2).sqrt * (2 + t ^ 2).sqrt)
  exact ⟨C, integralPosAux, fun _ ↦ vertIntBound xpos⟩
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
⊢ 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
⊢ VerticalIntegral (f x) σ = 0