English
If f is almost everywhere measurable with respect to the sum of measures m, then the map of the sum equals the sum of the maps: map f (sum m) = sum (map f (m i)).
Русский
Если f а.е.-измерима относительно суммы мер, тогда отображение по сумме равно сумме отображений: map f (sum m) = sum (map f (m i)).
LaTeX
$$$\mathrm{map}\, f\, (\mathrm{sum}\, m) = \mathrm{sum}\ (\lambda i, \mathrm{map}\, f\,(m\, i))$$$
Lean4
theorem map_sum {ι : Type*} {m : ι → Measure α} {f : α → β} (hf : AEMeasurable f (Measure.sum m)) :
Measure.map f (Measure.sum m) = Measure.sum (fun i ↦ Measure.map f (m i)) :=
by
ext s hs
rw [map_apply_of_aemeasurable hf hs, sum_apply₀ _ (hf.nullMeasurable hs), sum_apply _ hs]
have M i : AEMeasurable f (m i) := hf.mono_measure (le_sum m i)
simp_rw [map_apply_of_aemeasurable (M _) hs]
