IntervalIntegrable tactics?

Stream: Is there code for X?

[Alex Kontorovich]

Are there integrability tactics that make proving something like this less mind-numbingly tedious? Thanks!

import Mathlib

lemma integrability_aux {a b : ℝ} (a_lt_b : a < b) :
    IntervalIntegrable (fun (x : ℝ) ↦ (⌊x⌋ : ℂ) + 1 / 2 - x) MeasureTheory.volume a b := sorry

[Floris van Doorn]

docs#Continuous.intervalIntegrable + the tactic fun_prop?

[Floris van Doorn]

Oh, oops, I misread floor as abs.

[Floris van Doorn]

Do we have Measurable + Bounded range = Interval integrable? fun_prop can deal with Measurable (maybe with some lemmas about floor tagged), and bounded range is hopefully not too hard.

[Vincent Beffara]

You can cook it with docs#IntervalIntegrable.mono_fun' and docs#intervalIntegrable_const