setIntegral_condExp — Mathlib

English

Integrating condExp over a measurable set is the same as integrating the original function over that set under sigma-finite assumptions.

Русский

Интегрирование condExp по измеримому множеству даёт тот же интеграл, что и интеграл от исходной функции, при сигма-конечности.

LaTeX

$$$$\\int_s (\\mu[f|m])(x) \\, d\\mu(x) = \\int_s f(x) \\, d\\mu(x).$$$$

Lean4

/-- The integral of the conditional expectation `μ[f|hm]` over an `m`-measurable set is equal to
the integral of `f` on that set. -/
theorem setIntegral_condExp (hm : m ≤ m₀) [SigmaFinite (μ.trim hm)] (hf : Integrable f μ) (hs : MeasurableSet[m] s) :
    ∫ x in s, (μ[f|m]) x ∂μ = ∫ x in s, f x ∂μ :=
  by
  rw [setIntegral_congr_ae (hm s hs) ((condExp_ae_eq_condExpL1 hm f).mono fun x hx _ => hx)]
  exact setIntegral_condExpL1 hf hs

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