English
Let f be a nonnegative measurable function on β and g : α → β be measurable. Then the nonnegative integral with respect to the pushforward measure map g μ equals the nonnegative integral of f composed with g with respect to μ; i.e. ∫ f d(map g μ) = ∫ (f ∘ g) dμ.
Русский
Пусть f — неотрицимая измеримая функция на β, а g : α → β — измеримо. Тогда линеграл по образующему отображению сохраняется: ∫ f d(map g μ) = ∫ (f ∘ g) dμ.
LaTeX
$$$$ \int f\, d(map\ g\ μ) = \int (f\circ g)\, dμ, \quad \text{если } f \text{ измеримо и } g \text{ измеримо}.$$$$
Lean4
theorem lintegral_map {f : β → ℝ≥0∞} {g : α → β} (hf : Measurable f) (hg : Measurable g) :
∫⁻ a, f a ∂map g μ = ∫⁻ a, f (g a) ∂μ :=
by
rw [lintegral_eq_iSup_eapprox_lintegral hf]
simp only [← Function.comp_apply (f := f) (g := g)]
rw [lintegral_eq_iSup_eapprox_lintegral (hf.comp hg)]
congr with n : 1
convert SimpleFunc.lintegral_map _ hg
ext1 x; simp only [eapprox_comp hf hg, coe_comp]
