integral_simpleFunc_larger_space — Mathlib

English

If hm is a trimming of σ-algebras and f is a simple function, the integral with μ equals the integral with μ.trim hm.

Русский

Если hm – усечение сигма-алгебр, а f – простая функция, то интеграл по μ равен интегралу по μ.trim hm.

LaTeX

$$$\\int f\, d\\mu = \\int f\, d(\\mutrim)$$$

Lean4

theorem integral_simpleFunc_larger_space (hm : m ≤ m0) (f : @SimpleFunc β m F) (hf_int : Integrable f μ) :
    ∫ x, f x ∂μ = ∑ x ∈ @SimpleFunc.range β F m f, μ.real (f ⁻¹' { x }) • x :=
  by
  simp_rw [← f.coe_toLargerSpace_eq hm]
  rw [SimpleFunc.integral_eq_sum _ hf_int]
  congr 1

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