mathlib documentation

measure_theory.function.floor

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 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 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 {α : 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.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 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⌉₊)