English
The region between two a.e.-measurable functions on a null-measurable set is null-measurable; a version for Ico graph.
Русский
Область между двумя а.е.-измеримыми функциями на нулевой измеримой области нулевой мерой; версия с графиком нижней функции.
LaTeX
$$$\text{NullMeasurableSet}\{p: \alpha \times \mathbb{R} \mid p.1 \in s \wedge p.2 \in Ico(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 graph of the lower function. -/
theorem nullMeasurableSet_region_between_co (μ : Measure α) {f g : α → ℝ} (f_mble : AEMeasurable f μ)
(g_mble : AEMeasurable g μ) {s : Set α} (s_mble : NullMeasurableSet s μ) :
NullMeasurableSet {p : α × ℝ | p.1 ∈ s ∧ p.snd ∈ Ico (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
· exact nullMeasurableSet_lt measurable_snd.aemeasurable (by fun_prop)
