Theorems · Definition · measure theory

MeasureTheory.condLExp

{Ω : Type u_2} → {mΩ₀ : MeasurableSpace Ω} → MeasurableSpace Ω → MeasureTheory.Measure Ω → (Ω → ENNReal) → Ω → ENNReal

Conditional (Lebesgue) expectation of a function, with notation P⁻[X|mΩ]. It is defined as 0 if either ¬ mΩ ≤ mΩ₀ or hm : mΩ ≤ mΩ₀ but ¬ SigmaFinite (P.trim hm). One should typically not use the definition directly.

Defined in

Mathlib.MeasureTheory.Function.ConditionalLExpectation

Cited by

38 results in Mathlib

Foundations

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