integral_trim_ae — Mathlib

English

If φ is integrable and L preserves integrals under trimming, then the action commutes with trimming.

Русский

Если φ интегрируема и тримминг сохраняет интегралы, то действие сохраняет коммутативность с триммингом.

LaTeX

$$$\\int φ \\, dμ = \\int φ \\, dμtrim$$$

Lean4

theorem integral_trim_ae (hm : m ≤ m0) {f : β → G} (hf : AEStronglyMeasurable[m] f (μ.trim hm)) :
    ∫ x, f x ∂μ = ∫ x, f x ∂μ.trim hm :=
  by
  rw [integral_congr_ae (ae_eq_of_ae_eq_trim hf.ae_eq_mk), integral_congr_ae hf.ae_eq_mk]
  exact integral_trim hm hf.stronglyMeasurable_mk

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