Theorem: integrability_aux₁ (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
a b : ℝ
⊢ IntervalIntegrable (fun x => ↑⌊x⌋) MeasureTheory.volume a b
Tactic:
rw [intervalIntegrable_iff']
State after:
a b : ℝ
⊢ MeasureTheory.IntegrableOn (fun x => ↑⌊x⌋) [[a, b]] MeasureTheory.volume

State before:
a b : ℝ
⊢ MeasureTheory.IntegrableOn (fun x => ↑⌊x⌋) [[a, b]] MeasureTheory.volume
Tactic:
apply MeasureTheory.Measure.integrableOn_of_bounded ?_ ?_ integrability_aux₀
State after:
a b : ℝ
⊢ MeasureTheory.volume [[a, b]] ≠ ⊤

a b : ℝ
⊢ MeasureTheory.AEStronglyMeasurable (fun a => ↑⌊a⌋) MeasureTheory.volume

State before:
a b : ℝ
⊢ MeasureTheory.volume [[a, b]] ≠ ⊤
Tactic:
simp only [Real.volume_interval, ne_eq, ENNReal.ofReal_ne_top, not_false_eq_true]
State after:
no goals

State before:
a b : ℝ
⊢ MeasureTheory.AEStronglyMeasurable (fun a => ↑⌊a⌋) MeasureTheory.volume
Tactic:
apply Measurable.aestronglyMeasurable
State after:
case hf
a b : ℝ
⊢ Measurable fun a => ↑⌊a⌋

State before:
case hf
a b : ℝ
⊢ Measurable fun a => ↑⌊a⌋
Tactic:
apply Measurable.comp (by exact fun ⦃t⦄ _ ↦ trivial) Int.measurable_floor
State after:
no goals

State before:
a b : ℝ
⊢ Measurable IntCast.intCast
Tactic:
exact fun ⦃t⦄ _ ↦ trivial
State after:
no goals