integral_trim_simpleFunc — Mathlib

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

Похожие утверждения