ZetaAbelFractKernel.integrableOn_Ioi

theorem integrableOn_Ioi (s : ℂ) (hs : 0 < s.re) :    Integrable (fun u => zetaAbelFractKernel s u) (volume.restrict (Ioi (1 : ℝ))) := by  set ε : ℝ := s.re / 2  set g : ℝ → ℝ := fun u => u ^ (-1 - ε)  have hfm := aestronglyMeasurable s (Ioi (1 : ℝ)) measurableSet_Ioi  have hε : 0 < ε := half_pos hs  have hεle : ε ≤ s.re := half_le_self (le_of_lt hs)  have hbound : ∀ᵐ u ∂(volume.restrict (Ioi (1 : ℝ))), ‖zetaAbelFractKernel s u‖ ≤ g u :=    ae_restrict_iff' measurableSet_Ioi |>.2 <| ae_of_all _ fun u hu =>      (norm_zetaAbelFractKernel_le u (le_of_lt hu) s).trans        (Real.rpow_le_rpow_of_exponent_le (le_of_lt hu) (by linarith [hεle]))  simpa [IntegrableOn] using    IntegrableOn.mono' (integrableOn_Ioi_rpow_of_lt (by linarith) one_pos) hfm hbound