Measurability of ⌊x⌋ etc

In this file we prove that Int.floor, Int.ceil, Int.fract, Nat.floor, and Nat.ceil are measurable under some assumptions on the (semi)ring.

theorem Int.measurable_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [TopologicalSpace R] [OrderTopology R] [MeasurableSpace R] [OpensMeasurableSpace R] : Measurable floor

theorem Measurable.floor {α : Type u_1} {R : Type u_2} [MeasurableSpace α] [Ring R] [LinearOrder R] [FloorRing R] [TopologicalSpace R] [OrderTopology R] [MeasurableSpace R] [OpensMeasurableSpace R] {f : α → R} (hf : Measurable f) : Measurable fun (x : α) => ⌊f x⌋

theorem Int.measurable_ceil {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [TopologicalSpace R] [OrderTopology R] [MeasurableSpace R] [OpensMeasurableSpace R] : Measurable ceil

theorem Measurable.ceil {α : Type u_1} {R : Type u_2} [MeasurableSpace α] [Ring R] [LinearOrder R] [FloorRing R] [TopologicalSpace R] [OrderTopology R] [MeasurableSpace R] [OpensMeasurableSpace R] {f : α → R} (hf : Measurable f) : Measurable fun (x : α) => ⌈f x⌉

theorem measurable_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [TopologicalSpace R] [OrderTopology R] [MeasurableSpace R] [IsOrderedAddMonoid R] [BorelSpace R] : Measurable Int.fract

theorem Measurable.fract {α : Type u_1} {R : Type u_2} [MeasurableSpace α] [Ring R] [LinearOrder R] [FloorRing R] [TopologicalSpace R] [OrderTopology R] [MeasurableSpace R] [IsOrderedAddMonoid R] [BorelSpace R] {f : α → R} (hf : Measurable f) : Measurable fun (x : α) => Int.fract (f x)

theorem MeasurableSet.image_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [TopologicalSpace R] [OrderTopology R] [MeasurableSpace R] [IsOrderedAddMonoid R] [BorelSpace R] {s : Set R} (hs : MeasurableSet s) : MeasurableSet (Int.fract '' s)

theorem Nat.measurable_floor {R : Type u_2} [Semiring R] [LinearOrder R] [FloorSemiring R] [TopologicalSpace R] [OrderTopology R] [MeasurableSpace R] [OpensMeasurableSpace R] : Measurable floor

theorem Measurable.nat_floor {α : Type u_1} {R : Type u_2} [MeasurableSpace α] [Semiring R] [LinearOrder R] [FloorSemiring R] [TopologicalSpace R] [OrderTopology R] [MeasurableSpace R] [OpensMeasurableSpace R] {f : α → R} (hf : Measurable f) : Measurable fun (x : α) => ⌊f x⌋₊

theorem Nat.measurable_ceil {R : Type u_2} [Semiring R] [LinearOrder R] [FloorSemiring R] [TopologicalSpace R] [OrderTopology R] [MeasurableSpace R] [OpensMeasurableSpace R] : Measurable ceil

theorem Measurable.nat_ceil {α : Type u_1} {R : Type u_2} [MeasurableSpace α] [Semiring R] [LinearOrder R] [FloorSemiring R] [TopologicalSpace R] [OrderTopology R] [MeasurableSpace R] [OpensMeasurableSpace R] {f : α → R} (hf : Measurable f) : Measurable fun (x : α) => ⌈f x⌉₊