English
For ENNReal-valued functions, existence of almost disjoint measurable supersets yields a.e. measurability.
Русский
Для функций, значений ENNReal, существование почти раздельных измеримых супермножества допускает a.e. измеримость.
LaTeX
$$$$ \text{A.E. measurability from disjoint supersets} $$$$
Lean4
/-- 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. -/
theorem aemeasurable_of_exist_almost_disjoint_supersets {α : Type*} {m : MeasurableSpace α} (μ : Measure α)
(f : α → ℝ≥0∞)
(h :
∀ (p : ℝ≥0) (q : ℝ≥0),
p < q →
∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | (q : ℝ≥0∞) < f x} ⊆ v ∧ μ (u ∩ v) = 0) :
AEMeasurable f μ :=
by
obtain ⟨s, s_count, s_dense, _, s_top⟩ : ∃ s : Set ℝ≥0∞, s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ∞ ∉ s :=
ENNReal.exists_countable_dense_no_zero_top
have I : ∀ x ∈ s, x ≠ ∞ := fun x xs hx => s_top (hx ▸ xs)
apply MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets μ s s_count s_dense _
rintro p hp q hq hpq
lift p to ℝ≥0 using I p hp
lift q to ℝ≥0 using I q hq
exact h p q (ENNReal.coe_lt_coe.1 hpq)
