integral_condExp — Mathlib

English

The integral of condExp with respect to μ equals the integral of the original function over the whole space.

Русский

Интеграл condExp по μ равен интегралу исходной функции по всей области.

LaTeX

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

Lean4

theorem integral_condExp (hm : m ≤ m₀) [hμm : SigmaFinite (μ.trim hm)] : ∫ x, (μ[f|m]) x ∂μ = ∫ x, f x ∂μ :=
  by
  by_cases hf : Integrable f μ
  · suffices ∫ x in Set.univ, (μ[f|m]) x ∂μ = ∫ x in Set.univ, f x ∂μ by simp_rw [setIntegral_univ] at this; exact this
    exact setIntegral_condExp hm hf .univ
  simp only [condExp_of_not_integrable hf, Pi.zero_apply, integral_zero, integral_undef hf]

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