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}
[LinearOrderedRing R]
[FloorRing R]
[TopologicalSpace R]
[OrderTopology R]
[MeasurableSpace R]
[OpensMeasurableSpace R]
:
Measurable Int.floor
theorem
Measurable.floor
{α : Type u_1}
{R : Type u_2}
[MeasurableSpace α]
[LinearOrderedRing 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}
[LinearOrderedRing R]
[FloorRing R]
[TopologicalSpace R]
[OrderTopology R]
[MeasurableSpace R]
[OpensMeasurableSpace R]
:
Measurable Int.ceil
theorem
Measurable.ceil
{α : Type u_1}
{R : Type u_2}
[MeasurableSpace α]
[LinearOrderedRing 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}
[LinearOrderedRing R]
[FloorRing R]
[TopologicalSpace R]
[OrderTopology R]
[MeasurableSpace R]
[BorelSpace R]
:
Measurable Int.fract
theorem
Measurable.fract
{α : Type u_1}
{R : Type u_2}
[MeasurableSpace α]
[LinearOrderedRing R]
[FloorRing R]
[TopologicalSpace R]
[OrderTopology R]
[MeasurableSpace R]
[BorelSpace R]
{f : α → R}
(hf : Measurable f)
:
Measurable fun (x : α) => Int.fract (f x)
theorem
MeasurableSet.image_fract
{R : Type u_2}
[LinearOrderedRing R]
[FloorRing R]
[TopologicalSpace R]
[OrderTopology R]
[MeasurableSpace R]
[BorelSpace R]
{s : Set R}
(hs : MeasurableSet s)
:
MeasurableSet (Int.fract '' s)
theorem
Nat.measurable_floor
{R : Type u_2}
[LinearOrderedSemiring R]
[FloorSemiring R]
[TopologicalSpace R]
[OrderTopology R]
[MeasurableSpace R]
[OpensMeasurableSpace R]
:
Measurable Nat.floor
theorem
Measurable.nat_floor
{α : Type u_1}
{R : Type u_2}
[MeasurableSpace α]
[LinearOrderedSemiring 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}
[LinearOrderedSemiring R]
[FloorSemiring R]
[TopologicalSpace R]
[OrderTopology R]
[MeasurableSpace R]
[OpensMeasurableSpace R]
:
Measurable Nat.ceil
theorem
Measurable.nat_ceil
{α : Type u_1}
{R : Type u_2}
[MeasurableSpace α]
[LinearOrderedSemiring R]
[FloorSemiring R]
[TopologicalSpace R]
[OrderTopology R]
[MeasurableSpace R]
[OpensMeasurableSpace R]
{f : α → R}
(hf : Measurable f)
:
Measurable fun (x : α) => ⌈f x⌉₊