Theorems · Definition · measure theory

MeasureTheory.condExpIndL1

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

Conditional expectation of the indicator of a set, as a function in L1. Its value for sets which are not both measurable and of finite measure is not used: we set it to 0.

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Cited by

10 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceMeasureTheory.SigmaFinite