apply IntegrableOn.integrable ?_ |>.norm
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ IntegrableOn (fun x => ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) (Ioi ↑N) volume
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ IntegrableOn (fun a => (↑⌊a⌋ + 1 / 2 - ↑a) / ↑a ^ (↑σ + ↑t * I + 1)) (Ioi ↑N) volume