Perron.vertIntBoundLeft

@[blueprint  "vertIntBoundLeft"  (title := "vertIntBoundLeft")  (statement := /--  Let $x>1$ and $\sigma<-3/2$. Then  $$\left|  \int_{(\sigma)}\frac{x^s}{s(s+1)}ds\right| \leq    x^\sigma \int_\R\frac{1}{|(1/4+t ^ 2)(2+t ^ 2)|^{1/2}}dt.$$  -/)  (proof := /-- Triangle inequality and pointwise estimate. -/)  (latexEnv := "lemma")]lemma vertIntBoundLeft (xpos : 0 < x) :    ∃ C, ∀ (σ : ℝ) (_ : σ < -3 / 2), ‖VerticalIntegral' (f x) σ‖ ≤ C * x ^ σ := by   /- This proof is adapted from `vertIntBound` -/  use 1 / (2 * π) *    ‖(∫ (t : ℝ), 1 / ((4⁻¹ + t ^ 2).sqrt * (4⁻¹ + t ^ 2).sqrt : ℂ))‖  intro σ hσ  simp only [VerticalIntegral', smul_eq_mul, norm_mul]  rw [(by simp [pi_nonneg] : ‖1 / (2 * ↑π * I)‖ = 1 / (2 * π)), mul_assoc]  apply (mul_le_mul_iff_right₀ (by simp [pi_pos])).mpr  calc    _ = ‖∫ (t : ℝ), x ^ (σ + t * I) / ((σ + t * I) * (σ + t * I + 1))‖ := ?_    _ ≤ ∫ (t : ℝ), ‖x ^ (σ + t * I) / ((σ + t * I) * (σ + t * I + 1))‖ :=        norm_integral_le_integral_norm _    _ = ∫ (t : ℝ), x ^ σ / ‖((σ + t * I) * (σ + t * I + 1))‖ := ?_    _ = x ^ σ * ∫ (t : ℝ), 1 / (‖σ + t * I‖ * ‖σ + t * I + 1‖) := ?_    _ ≤ x ^ σ * ∫ (t : ℝ), 1 / ((4⁻¹ + t ^ 2).sqrt * (4⁻¹ + t ^ 2).sqrt) := ?_    _ ≤ _ := ?_  · simp [VerticalIntegral]  · congr with t    rw [norm_div, Complex.norm_cpow_eq_rpow_re_of_pos xpos, add_re, ofReal_re,      re_ofReal_mul, I_re, mul_zero, add_zero]  · simp_rw [div_eq_mul_inv, integral_const_mul, one_mul, norm_mul]  · gcongr x ^ σ * ?_    by_cases hint : Integrable fun (a : ℝ) ↦ 1 / (‖σ + ↑a * I‖ * ‖σ + ↑a * I + 1‖)    swap    · rw [integral_undef hint]      exact integral_nonneg <| fun t ↦ by simp only [Pi.zero_apply]; positivity    apply integral_mono hint    · have := integralPosAux' (4⁻¹) (4⁻¹) (by norm_num) (by norm_num)      contrapose! this      simp_rw [integral_undef this, le_rfl]    rw [Pi.le_def]    intro t    gcongr <;> apply sqrt_le_sqrt    · rw [normSq_add_mul_I, add_le_add_iff_right]; ring_nf; nlinarith    · rw [(by push_cast; ring : σ + t * I + 1 = ofReal (σ + 1) + t * I),        normSq_add_mul_I, add_le_add_iff_right]; ring_nf; nlinarith  · rw [mul_comm]    gcongr    · have : 0 ≤ ∫ (t : ℝ), 1 / (Real.sqrt (4⁻¹ + t ^ 2) * Real.sqrt (4⁻¹ + t ^ 2)) :=        by positivity      rw [← norm_of_nonneg this, ← Complex.norm_real]      apply le_of_eq; congr; norm_cast