Theorem: ZetaSum_aux1_5c (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
a b : ℝ
s : ℂ
⊢ let g := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1);
  AEStronglyMeasurable g (volume.restrict (Ι a b))
Tactic:
intro
State after:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ AEStronglyMeasurable g✝ (volume.restrict (Ι a b))

State before:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ AEStronglyMeasurable g✝ (volume.restrict (Ι a b))
Tactic:
refine (Measurable.div ?_ <| measurable_id.pow_const _).aestronglyMeasurable
State after:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ Measurable fun u => |↑⌊u⌋ + 1 / 2 - u|

State before:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ Measurable fun u => |↑⌊u⌋ + 1 / 2 - u|
Tactic:
refine _root_.continuous_abs.measurable.comp ?_
State after:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ Measurable fun u => ↑⌊u⌋ + 1 / 2 - u

State before:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ Measurable fun u => ↑⌊u⌋ + 1 / 2 - u
Tactic:
refine Measurable.add ?_ measurable_const |>.sub measurable_id
State after:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ Measurable fun u => ↑⌊u⌋

State before:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ Measurable fun u => ↑⌊u⌋
Tactic:
exact Measurable.comp (by exact fun _ _ ↦ trivial) Int.measurable_floor
State after:
no goals

State before:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ Measurable IntCast.intCast
Tactic:
exact fun _ _ ↦ trivial
State after:
no goals