English
For zero in β, the measurability of membership under the map s.indicator f corresponds to membership under the map f with the restricted measure μ|_s.
Русский
Пусть 0 принадлежит t; тогда принадлежность t под картой indicator эквивалентна принадлежности t под картой f с ограниченной мерой μ|_s.
LaTeX
$$$ t \\in \\operatorname{map}(s.indicator f) (ae \\mu) \\iff t \\in \\operatorname{map} f (ae (\\mu|_s)) $$$
Lean4
theorem mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem [Zero β] {t : Set β} (ht : (0 : β) ∈ t)
(hs : MeasurableSet s) : t ∈ Filter.map (s.indicator f) (ae μ) ↔ t ∈ Filter.map f (ae <| μ.restrict s) := by
classical
simp_rw [mem_map, mem_ae_iff]
rw [Measure.restrict_apply' hs, Set.indicator_preimage, Set.ite]
simp_rw [Set.compl_union, Set.compl_inter]
change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0
simp only [ht, ← Set.compl_eq_univ_diff, compl_compl, if_true, Set.preimage_const]
simp_rw [Set.union_inter_distrib_right, Set.compl_inter_self s, Set.union_empty]
