Perron.tendsto_zero_Lower

@[blueprint  "tendsto_zero_Lower"  (title := "tendsto-zero-Lower")  (statement := /--  Let $x>0$ and $\sigma',\sigma''\in\R$. Then  $$\int_{\sigma'}^{\sigma''}\frac{x^{\sigma+it}}{(\sigma+it)(1+\sigma + it)}d\sigma$$  goes to $0$ as $t\to-\infty$.  -/)  (proof := /-- The numerator is bounded and the denominator tends to infinity. -/)  (latexEnv := "lemma")]lemma tendsto_zero_Lower (xpos : 0 < x) (σ' σ'' : ℝ) :    Tendsto (fun (t : ℝ) ↦ ∫ (σ : ℝ) in σ'..σ'', f x (σ + t * I)) atBot (𝓝 0) := by   have hcast : (fun (y : ℝ) ↦ 1 / y ^ 2) =ᶠ[atBot] fun y ↦ (-y) ^ (-2 : ℝ) := by    filter_upwards [Iic_mem_atBot 0] with y hy using      by rw [rpow_neg (neg_nonneg.mpr hy), inv_eq_one_div, rpow_two, neg_sq]  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