filter_upwards [mem_atTop (N + 1 : ℝ)] with t ht
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ ∀ᶠ (c : ℝ) in atTop, (fun t => ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) c ≤ ↑N ^ (-σ) / σ
case h
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
⊢ ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ ↑N ^ (-σ) / σ