Theorems · Theorem · measure theory

MeasureTheory.lintegral_condLExp

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

Defined in

Mathlib.MeasureTheory.Function.ConditionalLExpectation

Cited by

5 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SigmaFinite