apply intervalIntegral_tendsto_integral_Ioi (μ := volume) (l := atTop) (b := id)
  (f := fun (x : ℝ) ↦ ‖(⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ (σ + t * I + 1)‖) N ?_ ?_ |>.congr' ?_
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ Tendsto (fun t => ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) atTop
    (𝓝 (∫ (a : ℝ) in Ioi ↑N, ‖(↑⌊a⌋ + 1 / 2 - ↑a) / ↑a ^ (↑σ + ↑t * I + 1)‖))
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ (fun i => ∫ (x : ℝ) in ↑N..id i, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) =ᶠ[atTop] fun t =>
    ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖

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 < σ
⊢ Tendsto id atTop atTop