English
Let g: X → Y be a measurable mapping and f: Y → E. Then the integral over s with respect to μ.map g equals the integral over the preimage g^{-1}(s) of f(g(x)).
Русский
Пусть g: X → Y измеримо, f: Y → E. Тогда интеграл по s для меры μ.map g равен интегралу по предобразу g^{-1}(s) от f(g(x)).
LaTeX
$$$$ \\int_{y \\in s} f(y) \\, d(\\mu \\circ g^{-1})(y) = \\int_{x \\in g^{-1}(s)} f(g(x)) \\, d\\mu(x) $$$$
Lean4
theorem setIntegral_map {Y} [MeasurableSpace Y] {g : X → Y} {f : Y → E} {s : Set Y} (hs : MeasurableSet s)
(hf : AEStronglyMeasurable f (Measure.map g μ)) (hg : AEMeasurable g μ) :
∫ y in s, f y ∂Measure.map g μ = ∫ x in g ⁻¹' s, f (g x) ∂μ :=
by
rw [Measure.restrict_map_of_aemeasurable hg hs,
integral_map (hg.mono_measure Measure.restrict_le_self) (hf.mono_measure _)]
exact Measure.map_mono_of_aemeasurable Measure.restrict_le_self hg
