English
Let s be a measurable set. Then the a.e.-measurability of the indicator function s.indicator f with respect to μ is equivalent to the a.e.-measurability of f with respect to μ.restrict s.
Русский
Для измеримого множества s а.е.-измеримость функции-индикатора s.indicator f относительно μ эквивалентна а.е.-измеримости f относительно μ.restrict s.
LaTeX
$$$\mathrm{AEMeasurable}(\mathrm{indicator}\ s\ f,\ \mu) \iff \mathrm{AEMeasurable}(f,\ \mu\restriction s)$$$
Lean4
theorem aemeasurable_indicator_iff {s} (hs : MeasurableSet s) :
AEMeasurable (indicator s f) μ ↔ AEMeasurable f (μ.restrict s) :=
by
constructor
· intro h
exact (h.mono_measure Measure.restrict_le_self).congr (indicator_ae_eq_restrict hs)
· intro h
refine ⟨indicator s (h.mk f), h.measurable_mk.indicator hs, ?_⟩
have A : s.indicator f =ᵐ[μ.restrict s] s.indicator (AEMeasurable.mk f h) :=
(indicator_ae_eq_restrict hs).trans (h.ae_eq_mk.trans <| (indicator_ae_eq_restrict hs).symm)
have B : s.indicator f =ᵐ[μ.restrict sᶜ] s.indicator (AEMeasurable.mk f h) :=
(indicator_ae_eq_restrict_compl hs).trans (indicator_ae_eq_restrict_compl hs).symm
exact ae_of_ae_restrict_of_ae_restrict_compl _ A B
