intro u hu
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ ∀ (a : ℝ),
    ↑N ≤ a →
      ∫ (x : ℝ) in ↑N..id a, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ =
        ∫ (x : ℝ) in ↑N..a, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑a * I + 1)‖
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
⊢ ∫ (x : ℝ) in ↑N..id u, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ =
    ∫ (x : ℝ) in ↑N..u, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑u * I + 1)‖