intro
a b : ℝ
s : ℂ
⊢ let g := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1);
  AEStronglyMeasurable g (volume.restrict (Ι a b))
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ AEStronglyMeasurable g✝ (volume.restrict (Ι a b))