Measurability of ⌊x⌋ etc #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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}
[linear_ordered_ring R]
[floor_ring R]
[topological_space R]
[order_topology R]
[measurable_space R]
[opens_measurable_space R] :
@[measurability]
theorem
measurable.floor
{α : Type u_1}
{R : Type u_2}
[measurable_space α]
[linear_ordered_ring R]
[floor_ring R]
[topological_space R]
[order_topology R]
[measurable_space R]
[opens_measurable_space R]
{f : α → R}
(hf : measurable f) :
measurable (λ (x : α), ⌊f x⌋)
theorem
int.measurable_ceil
{R : Type u_2}
[linear_ordered_ring R]
[floor_ring R]
[topological_space R]
[order_topology R]
[measurable_space R]
[opens_measurable_space R] :
@[measurability]
theorem
measurable.ceil
{α : Type u_1}
{R : Type u_2}
[measurable_space α]
[linear_ordered_ring R]
[floor_ring R]
[topological_space R]
[order_topology R]
[measurable_space R]
[opens_measurable_space R]
{f : α → R}
(hf : measurable f) :
measurable (λ (x : α), ⌈f x⌉)
theorem
measurable_fract
{R : Type u_2}
[linear_ordered_ring R]
[floor_ring R]
[topological_space R]
[order_topology R]
[measurable_space R]
[borel_space R] :
@[measurability]
theorem
measurable.fract
{α : Type u_1}
{R : Type u_2}
[measurable_space α]
[linear_ordered_ring R]
[floor_ring R]
[topological_space R]
[order_topology R]
[measurable_space R]
[borel_space R]
{f : α → R}
(hf : measurable f) :
measurable (λ (x : α), int.fract (f x))
theorem
measurable_set.image_fract
{R : Type u_2}
[linear_ordered_ring R]
[floor_ring R]
[topological_space R]
[order_topology R]
[measurable_space R]
[borel_space R]
{s : set R}
(hs : measurable_set s) :
theorem
nat.measurable_floor
{R : Type u_2}
[linear_ordered_semiring R]
[floor_semiring R]
[topological_space R]
[order_topology R]
[measurable_space R]
[opens_measurable_space R] :
@[measurability]
theorem
measurable.nat_floor
{α : Type u_1}
{R : Type u_2}
[measurable_space α]
[linear_ordered_semiring R]
[floor_semiring R]
[topological_space R]
[order_topology R]
[measurable_space R]
[opens_measurable_space R]
{f : α → R}
(hf : measurable f) :
measurable (λ (x : α), ⌊f x⌋₊)
theorem
nat.measurable_ceil
{R : Type u_2}
[linear_ordered_semiring R]
[floor_semiring R]
[topological_space R]
[order_topology R]
[measurable_space R]
[opens_measurable_space R] :
@[measurability]
theorem
measurable.nat_ceil
{α : Type u_1}
{R : Type u_2}
[measurable_space α]
[linear_ordered_semiring R]
[floor_semiring R]
[topological_space R]
[order_topology R]
[measurable_space R]
[opens_measurable_space R]
{f : α → R}
(hf : measurable f) :
measurable (λ (x : α), ⌈f x⌉₊)