English
The region between two almost everywhere measurable functions on a null-measurable set is null-measurable.
Русский
Область между двумя а.е.-измеримыми функциями на нулевом множесте измерима нулевой мерой.
LaTeX
$$$\text{NullMeasurableSet}\{p:\alpha \times \mathbb{R} \mid p.1 \in s \wedge p.2 \in Ioo(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. -/
theorem nullMeasurableSet_regionBetween (μ : Measure α) {f g : α → ℝ} (f_mble : AEMeasurable f μ)
(g_mble : AEMeasurable g μ) {s : Set α} (s_mble : NullMeasurableSet s μ) :
NullMeasurableSet {p : α × ℝ | p.1 ∈ s ∧ p.snd ∈ Ioo (f p.fst) (g p.fst)} (μ.prod volume) :=
by
refine NullMeasurableSet.inter (s_mble.preimage quasiMeasurePreserving_fst) (NullMeasurableSet.inter ?_ ?_)
· exact nullMeasurableSet_lt (by fun_prop) measurable_snd.aemeasurable
· exact nullMeasurableSet_lt measurable_snd.aemeasurable (by fun_prop)
