Perron.vertIntBound

@[blueprint  "vertIntBound"  (title := "vertIntBound")  (statement := /--  Let $x>0$ and $\sigma>1$. Then  $$\left|  \int_{(\sigma)}\frac{x^s}{s(s+1)}ds\right| \leq    x^\sigma \int_\R\frac{1}{|(1+t ^ 2)(2+t ^ 2)|^{1/2}}dt.$$  -/)  (proof := /-- Triangle inequality and pointwise estimate. -/)  (latexEnv := "lemma")]lemma vertIntBound (xpos : 0 < x) (σ_gt_one : 1 < σ) :    ‖VerticalIntegral (f x) σ‖ ≤      x ^ σ * ∫ (t : ℝ), 1 / ((1 + t ^ 2).sqrt * (2 + t ^ 2).sqrt) := by  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 / ((1 + t ^ 2).sqrt * (2 + t ^ 2).sqrt) :=        mul_le_mul_of_nonneg_left ?_ (rpow_nonneg xpos.le _)  · simp [VerticalIntegral]  · simp [Complex.norm_cpow_eq_rpow_re_of_pos xpos]  · simp [integral_const_mul, div_eq_mul_inv]  · by_cases hint : Integrable fun (a : ℝ) ↦ 1 / (‖σ + a * I‖ * ‖σ + a * I + 1‖)    swap    · rw [integral_undef hint]; exact integral_nonneg <| fun t ↦ by positivity    conv => rhs; rhs; intro a; rhs    apply integral_mono hint    · have := integralPosAux      contrapose! this      simp_rw [integral_undef this, le_rfl]    rw [Pi.le_def]    intro t    gcongr <;> apply sqrt_le_sqrt    · simp_rw [normSq_add_mul_I, add_le_add_iff_right, one_le_pow₀ σ_gt_one.le]    · rw [add_right_comm, ← ofReal_one, ← ofReal_add, normSq_add_mul_I, add_le_add_iff_right]      nlinarith  rfl