Perron.isIntegrable

@[blueprint "isIntegrable"  (title := "isIntegrable")  (statement := /--  Let $x>0$ and $\sigma\in\R$. Then  $$\int_{\R}\frac{x^{\sigma+it}}{(\sigma+it)(1+\sigma + it)}dt$$  is integrable.  -/)  (latexEnv := "lemma")]lemma isIntegrable (xpos : 0 < x) (σ_ne_zero : σ ≠ 0) (σ_ne_neg_one : σ ≠ -1) :    Integrable fun (t : ℝ) ↦ f x (σ + t * I) := by  /-- By \ref{isHolomorphicOn}, $f$ is continuous, so it is integrable on any interval.-/  have : Continuous (fun (y : ℝ) ↦ f x (σ + y * I)) := by    refine (isHolomorphicOn xpos).continuousOn.comp_continuous (by continuity) fun x ↦      not_or.mpr ?_    simp [Complex.ext_iff, σ_ne_zero, σ_ne_neg_one]  /-- Also, $|f(x)| = \Theta(x^{-2})$ as $x\to\infty$, -/  refine this.locallyIntegrable.integrable_of_isBigO_atTop_of_norm_isNegInvariant    (univ_mem' fun y ↦ ?_) (isTheta xpos).2.isBigO ⟨Ioi 1, Ioi_mem_atTop 1, ?_⟩  · /-- and $|f(-x)| = \Theta(x^{-2})$ as $x\to\infty$. -/    change ‖f x (↑σ + ↑y * I)‖ = ‖f x (↑σ + ↑(-y) * I)‖    have : (↑σ + ↑(-y) * I) = conj (↑σ + ↑y * I) := Complex.ext (by simp) (by simp)    simp_rw [this, map_conj xpos.le, norm_conj]  · /-- Since $g(x) = x^{-2}$ is integrable on $[a,\infty)$ for any $a>0$, we conclude. -/    refine integrableOn_Ioi_rpow_of_lt (show (-2 : ℝ) < -1 by norm_num)      (show (0 : ℝ) < 1 by norm_num) |>.congr_fun (fun y hy ↦ ?_) measurableSet_Ioi    have hy0 : (0 : ℝ) < y := (show (0 : ℝ) < 1 by norm_num).trans hy    change (y : ℝ) ^ (-2 : ℝ) = 1 / y ^ 2    rw [eq_div_iff (pow_ne_zero 2 hy0.ne'), ← rpow_natCast y 2, ← rpow_add hy0]    norm_num