exact fun x hx ↦ ZetaSum_aux1_4' x (ZetaSum_aux1_1 apos a_lt_b hx) s
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]]
no goals