ENNReal.aemeasurable_of_exist_almost_disjoint_supersets
theorem ENNReal.aemeasurable_of_exist_almost_disjoint_supersets :
∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal),
(∀ (p q : NNReal),
p < q →
∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0) →
AEMeasurable f μ
The theorem states that if a function `f` maps from an arbitrary type α to nonnegative real numbers extended with positive infinity, and for any pair of finite nonnegative real numbers `p` and `q` where `p` is less than `q`, there exist two measurable supersets `u` and `v` such that the set of `f` values less than `p` is contained in `u`, the set of `f` values greater than `q` is contained in `v`, and the intersection of `u` and `v` has measure zero, then the function `f` is almost everywhere measurable. In other words, this theorem provides a condition involving the relationship between the level sets of the function and certain measurable sets that guarantees that the function is almost everywhere measurable.
More concisely: If a function from an arbitrary type to nonnegative real numbers extends the real line with positive infinity, and for any finite real numbers p < q, there exist measurable sets u and v such that the sublevel sets {x : f(x) < p} are contained in u, the superlevel sets {x : f(x) > q} are contained in v, and the intersection of u and v has measure zero, then f is almost everywhere measurable.
|
MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets
theorem MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets :
∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {β : Type u_2} [inst : CompleteLinearOrder β]
[inst_1 : DenselyOrdered β] [inst_2 : TopologicalSpace β] [inst_3 : OrderTopology β]
[inst_4 : SecondCountableTopology β] [inst_5 : MeasurableSpace β] [inst_6 : BorelSpace β] (s : Set β),
s.Countable →
Dense s →
∀ (f : α → β),
(∀ p ∈ s,
∀ q ∈ s,
p < q →
∃ u v,
MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0) →
AEMeasurable f μ
The theorem states that if a function `f` mapping from `α` to `β` has the property that for each pair of distinct values `p` and `q` from a countable and dense set `s` in `β`, the level sets `{f < p}` and `{q < f}` have measurable supersets that are disjoint except for a set of measure zero, then `f` is almost everywhere measurable. Here, `{f < p}` denotes the set of points in `α` where the function `f` takes a value less than `p`, and `{q < f}` denotes the set of points where `f` takes a value greater than `q`. This condition only needs to hold for `p` and `q` in a countable dense set in `β`, not for all `p` and `q` in `β`. The space `β` is assumed to be a complete linear ordered topological space with a second countable, Borel measurable space structure. The measure on `α` is denoted by `μ`.
More concisely: If a function from a measurable space to a complete, linear ordered, second countable topological space with a Borel measurable structure has measurable supersets for the level sets of distinct values in a countable dense set such that these sets have measure zero intersection, then the function is almost everywhere measurable.
|