apply MeasureTheory.Integrable.bdd_mul ?_ ?_
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ MeasureTheory.IntegrableOn (fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) (Ioi ↑N) MeasureTheory.volume
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ∃ C, ∀ (x : ℝ), ‖↑⌊x⌋ + 1 / 2 - ↑x‖ ≤ C

N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ MeasureTheory.Integrable (fun x => ↑x ^ (-(s + 1))) (MeasureTheory.volume.restrict (Ioi ↑N))

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))