English
The region between two almost everywhere measurable functions on a null-measurable set is null-measurable; a version for Icc (closed-closed) region.
Русский
Область между двумя а.е.-измеримыми функциями на нулевой измеримой области, область между Icc.
LaTeX
$$$\text{NullMeasurableSet}\{p: \alpha \times \mathbb{R} \mid p.1 \in s \wedge p.2 \in Icc(f(p.1),g(p.1))\}(\mu.\text{prod volume})$$$
Lean4
/-- The region between two a.e.-measurable functions on a null-measurable set is null-measurable;
a version for the region together with the graphs of both functions. -/
theorem nullMeasurableSet_region_between_cc (μ : Measure α) {f g : α → ℝ} (f_mble : AEMeasurable f μ)
(g_mble : AEMeasurable g μ) {s : Set α} (s_mble : NullMeasurableSet s μ) :
NullMeasurableSet {p : α × ℝ | p.1 ∈ s ∧ p.snd ∈ Icc (f p.fst) (g p.fst)} (μ.prod volume) :=
by
refine NullMeasurableSet.inter (s_mble.preimage quasiMeasurePreserving_fst) (NullMeasurableSet.inter ?_ ?_)
· change NullMeasurableSet {p : α × ℝ | f p.fst ≤ p.snd} (μ.prod volume)
rw [show {p : α × ℝ | f p.fst ≤ p.snd} = {p : α × ℝ | p.snd < f p.fst}ᶜ
by
ext p
simp only [mem_setOf_eq, mem_compl_iff, not_lt]]
exact (nullMeasurableSet_lt measurable_snd.aemeasurable (by fun_prop)).compl
· change NullMeasurableSet {p : α × ℝ | p.snd ≤ g p.fst} (μ.prod volume)
rw [show {p : α × ℝ | p.snd ≤ g p.fst} = {p : α × ℝ | g p.fst < p.snd}ᶜ
by
ext p
simp only [mem_setOf_eq, mem_compl_iff, not_lt]]
exact (nullMeasurableSet_lt (by fun_prop) measurable_snd.aemeasurable).compl
