Theorems · Definition · measure theory

MeasureTheory.condExpIndSMul

{α : Type u_1} →
  {G : Type u_5} →
    [inst : NormedAddCommGroup G] →
      {m m0 : MeasurableSpace α} →
        {μ : MeasureTheory.Measure α} →
          {s : Set α} → [NormedSpace ℝ G] → m ≤ m0 → MeasurableSet s → μ s ≠ ⊤ → G → ↥(MeasureTheory.Lp G 2 μ)

Conditional expectation of the indicator of a measurable set with finite measure, in L2.

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Cited by

19 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace