Theorem: ZetaSum_aux1_4 (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
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
Tactic:
apply intervalIntegral.integral_congr
State after:
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]]

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