ZetaAbelFractKernel.intervalIntegrable

lemma intervalIntegrable (s : ℂ) {a b : ℝ} (ha : 1 ≤ a) (hab : a ≤ b) :    IntervalIntegrable (fun u => zetaAbelFractKernel s u) volume a b := by  let μ := volume.restrict (Icc a b)  set g : ℝ → ℝ := fun u => ‖(u : ℂ) ^ (-s - 1)‖  have hmeas := aestronglyMeasurable s (Icc a b) measurableSet_Icc  have hbound_ae : ∀ᵐ u ∂μ, ‖zetaAbelFractKernel s u‖ ≤ g u := by    refine (ae_restrict_iff' measurableSet_Icc).2 (ae_of_all _ ?_)    intro u huIcc    have hu0 : 0 < u := lt_of_lt_of_le one_pos (ha.trans huIcc.1)    have hg_eq : g u = u ^ (-s.re - 1) := by      simp [g, Complex.norm_cpow_eq_rpow_re_of_pos hu0, sub_eq_add_neg]    exact (norm_zetaAbelFractKernel_le u (ha.trans huIcc.1) s).trans (le_of_eq hg_eq.symm)  have hg : Integrable g μ := by    simpa [μ, g] using!      (Complex.continuousOn_ofReal_cpow (ha := one_pos.trans_le ha)).norm.integrableOn_compact        isCompact_Icc  have hf0 : Integrable (fun _ : ℝ => (0 : ℂ)) μ := by simp [μ]  exact (intervalIntegrable_iff_integrableOn_Icc_of_le hab).2 <|    integrable_of_norm_sub_le hmeas hf0 hg      (hbound_ae.mono fun u hu => by simpa [sub_eq_add_neg, μ, g] using hu)