refine Measurable.add ?_ measurable_const |>.sub (by fun_prop) |>.aestronglyMeasurable
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ MeasureTheory.AEStronglyMeasurable (fun x => ↑⌊x⌋ + 1 / 2 - ↑x) (MeasureTheory.volume.restrict (Ioi ↑N))
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Measurable fun x => ↑⌊x⌋