exact isBigO_sup.mp (horizontal_integral_isBigO xpos σ' σ'' volume)
  |>.1.trans_eventuallyEq hcast |>.trans_tendsto
  <| tendsto_rpow_neg_atTop (by norm_num) |>.comp tendsto_neg_atBot_atTop
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
hcast : (fun y => 1 / y ^ 2) =ᶠ[atBot] fun y => (-y) ^ (-2)
⊢ Tendsto (fun t => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑t * I)) atBot (𝓝 0)
no goals