English
For any measurable set s, AEStronglyMeasurable(indicator s f) μ holds if and only if AEStronglyMeasurable f on μ restricted to s.
Русский
Для всякого измеримого множества s равенство AEStronglyMeasurable(indicator s f) μ эквивалентно AEStronglyMeasurable f на μ, ограниченной до s.
LaTeX
$$$AEStronglyMeasurable(indicator\,s\,f, \mu) \iff AEStronglyMeasurable(f, \mu|_s)$$$
Lean4
theorem _root_.aestronglyMeasurable_indicator_iff [Zero β] {s : Set α} (hs : MeasurableSet s) :
AEStronglyMeasurable (indicator s f) μ ↔ AEStronglyMeasurable 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.stronglyMeasurable_mk.indicator hs, ?_⟩
have A : s.indicator f =ᵐ[μ.restrict s] s.indicator (h.mk f) :=
(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 (h.mk f) :=
(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
