apply intervalIntegral.integral_congr
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
⊢ ∫ (x : ℝ) in a..b, ‖(↑⌊x⌋ + ↑1 / 2 - ↑x) / ↑x ^ (s + 1)‖ = ∫ (x : ℝ) in a..b, |↑⌊x⌋ + 1 / 2 - x| / x ^ (s + 1).re
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
⊢ EqOn (fun x => ‖(↑⌊x⌋ + ↑1 / 2 - ↑x) / ↑x ^ (s + 1)‖) (fun x => |↑⌊x⌋ + 1 / 2 - x| / x ^ (s + 1).re) [[a, b]]