Measurability criterion for ennreal-valued functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Consider a function f : α → ℝ≥0∞. If the level sets {f < p} and {q < f} have measurable supersets which are disjoint up to measure zero when p and q are finite numbers satisfying p < q, then f is almost-everywhere measurable. This is proved in ennreal.ae_measurable_of_exist_almost_disjoint_supersets, and deduced from an analogous statement for any target space which is a complete linear dense order, called measure_theory.ae_measurable_of_exist_almost_disjoint_supersets.

Note that it should be enough to assume that the space is a conditionally complete linear order, but the proof would be more painful. Since our only use for now is for ℝ≥0∞, we keep it as simple as possible.

source

theorem measure_theory.ae_measurable_of_exist_almost_disjoint_supersets {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) {β : Type u_2} [complete_linear_order β] [densely_ordered β] [topological_space β] [order_topology β] [topological_space.second_countable_topology β] [measurable_space β] [borel_space β] (s : set β) (s_count : s.countable) (s_dense : dense s) (f : α → β) (h : ∀ (p : β), p ∈ s → ∀ (q : β), q ∈ s → p < q → (∃ (u v : set α), measurable_set u ∧ measurable_set v ∧ {x : α | f x < p} ⊆ u ∧ {x : α | q < f x} ⊆ v ∧ ⇑μ (u ∩ v) = 0)) :

ae_measurable f μ

If a function f : α → β is such that the level sets {f < p} and {q < f} have measurable supersets which are disjoint up to measure zero when p < q, then f is almost-everywhere measurable. It is even enough to have this for p and q in a countable dense set.

source

theorem ennreal.ae_measurable_of_exist_almost_disjoint_supersets {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) (f : α → ennreal) (h : ∀ (p q : nnreal), p < q → (∃ (u v : set α), measurable_set u ∧ measurable_set v ∧ {x : α | f x < ↑p} ⊆ u ∧ {x : α | ↑q < f x} ⊆ v ∧ ⇑μ (u ∩ v) = 0)) :

ae_measurable f μ

If a function f : α → ℝ≥0∞ is such that the level sets {f < p} and {q < f} have measurable supersets which are disjoint up to measure zero when p and q are finite numbers satisfying p < q, then f is almost-everywhere measurable.