English
Let φ: α→β be a measurable map and f: β→G; then the integral with respect to the pushforward map equals the integral of f∘φ with respect to μ, provided suitable measurability.
Русский
Пусть φ: α→β измеримо, f: β→G; тогда интеграл по мере map φ μ равен интегралу f∘φ по μ при подходящей измеримости.
LaTeX
$$$$\int y, f(y) \partial(Measure.map φ \mu) = \int x, f(φ(x)) \partial\mu.$$$$
Lean4
theorem integral_map_of_stronglyMeasurable {β} [MeasurableSpace β] {φ : α → β} (hφ : Measurable φ) {f : β → G}
(hfm : StronglyMeasurable f) : ∫ y, f y ∂Measure.map φ μ = ∫ x, f (φ x) ∂μ :=
by
by_cases hG : CompleteSpace G; swap
· simp [integral, hG]
by_cases hfi : Integrable f (Measure.map φ μ); swap
· rw [integral_undef hfi, integral_undef]
exact fun hfφ => hfi ((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).2 hfφ)
borelize G
have : SeparableSpace (range f ∪ {0} : Set G) := hfm.separableSpace_range_union_singleton
refine
tendsto_nhds_unique (tendsto_integral_approxOn_of_measurable_of_range_subset hfm.measurable hfi _ Subset.rfl) ?_
convert
tendsto_integral_approxOn_of_measurable_of_range_subset (hfm.measurable.comp hφ)
((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).1 hfi) (range f ∪ {0})
(union_subset_union_left {0} (range_comp_subset_range φ f)) using
1
ext1 i
simp only [SimpleFunc.integral_eq, hφ, SimpleFunc.measurableSet_preimage, map_measureReal_apply, ← preimage_comp]
refine (Finset.sum_subset (SimpleFunc.range_comp_subset_range _ hφ) fun y _ hy => ?_).symm
rw [SimpleFunc.mem_range, ← Set.preimage_singleton_eq_empty, SimpleFunc.coe_comp] at hy
rw [hy]
simp
