Theorems · Definition · measure theory

MeasureTheory.condExpL2

{α : Type u_1} →
  (E : Type u_2) →
    (𝕜 : Type u_7) →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [CompleteSpace E] →
              {m m0 : MeasurableSpace α} →
                {μ : MeasureTheory.Measure α} →
                  m ≤ m0 → ↥(MeasureTheory.Lp E 2 μ) →L[𝕜] ↥(MeasureTheory.lpMeas E 𝕜 m 2 μ)

Conditional expectation of a function in L2 with respect to a sigma-algebra

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Cited by

36 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceCompleteSpace