English
If φ is AEStronglyMeasurable and integrable, trimming preserves integrals pointwise for adjusted φ.
Русский
Если φ является AEStronglyMeasurable и интегрируема, усечение сохраняет интегралы.
LaTeX
$$$\\int φ \\, dμ = \\int φ \\, dμ.trim hm$$$
Lean4
theorem integral_trim_simpleFunc (hm : m ≤ m0) (f : @SimpleFunc β m F) (hf_int : Integrable f μ) :
∫ x, f x ∂μ = ∫ x, f x ∂μ.trim hm :=
by
have hf : StronglyMeasurable[m] f := @SimpleFunc.stronglyMeasurable β F m _ f
have hf_int_m := hf_int.trim hm hf
rw [integral_simpleFunc_larger_space (le_refl m) f hf_int_m, integral_simpleFunc_larger_space hm f hf_int]
congr with x
simp only [measureReal_def]
congr 2
exact (trim_measurableSet_eq hm (@SimpleFunc.measurableSet_fiber β F m f x)).symm