Theorems · Theorem · measure theory

MeasureTheory.setLIntegral_condLExp

∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (hm : mΩ ≤ mΩ₀) (P : MeasureTheory.Measure Ω)
  [hσ : MeasureTheory.SigmaFinite (P.trim hm)] (X : Ω → ENNReal) {s : Set Ω},
  MeasurableSet s → ∫⁻ (ω : Ω) in s, P⁻[X | mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P

The (Lebesgue) integral of the conditional (Lebesgue) expectation P⁻[X|mΩ] over an mΩ-measurable set is equal to the integral of X on that set.

Defined in

Mathlib.MeasureTheory.Function.ConditionalLExpectation

Cited by

8 results in Mathlib

Foundations

Depth 216 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.SigmaFinite