Theorems · Definition · measure theory

MeasureTheory.condExpL1

{α : Type u_1} →
  {F' : Type u_3} →
    [inst : NormedAddCommGroup F'] →
      [NormedSpace ℝ F'] →
        {m m0 : MeasurableSpace α} →
          (hm : m ≤ m0) →
            (μ : MeasureTheory.Measure α) →
              [MeasureTheory.SigmaFinite (μ.trim hm)] → (α → F') → ↥(MeasureTheory.Lp F' 1 μ)

Conditional expectation of a function, in L1. Its value is 0 if the function is not integrable. The function-valued condExp should be used instead in most cases.

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Cited by

26 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceMeasureTheory.SigmaFinite