eventually filter with measure restriction

Stream: Is there code for X?

[Alex Kontorovich]

Any suggestions for how to prove the below?

import Mathlib

open Interval

example {a b : ℝ} (a_lt_b : a < b) :
    ∀ᵐ (x : ℝ) ∂MeasureTheory.Measure.restrict MeasureTheory.volume [[a, b]],
      ‖(⌊x⌋ : ℂ)‖ ≤ b := by
  sorry

That is, for almost all (in fact, all) x with respect to the restriction of Lebesgue measure to [[a,b]], the floor of x (coerced into ℂ for some annoying reason) has norm at most b. How can I filter_upwards in such a way to retain the fact that x is in [[a, b]]? Thanks!

[Rémy Degenne]

docs#MeasureTheory.ae_restrict_iff (or docs#MeasureTheory.ae_restrict_iff') could be useful here to answer the question "how can I filter_upwards in such a way to retain the fact that x is in [[a, b]]?"

[Rémy Degenne]

import Mathlib

open Interval MeasureTheory

example {a b : ℝ} (a_lt_b : a < b) :
    ∀ᵐ (x : ℝ) ∂volume.restrict [[a, b]], ‖(⌊x⌋ : ℂ)‖ ≤ b := by
  rw [ae_restrict_iff']
  swap; · exact measurableSet_Icc
  refine ae_of_all _ (fun x hx ↦ ?_)
  -- need 0 ≤ a ?
  sorry

[Alex Kontorovich]

Great thanks!!