Theorems · Theorem · measure theory

MeasureTheory.setIntegral_condExpIndSMul

∀ {α : Type u_1} {G' : Type u_6} [inst : NormedAddCommGroup G'] [inst_1 : NormedSpace ℝ G'] [CompleteSpace G']
  {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} {hm : m ≤ m0},
  MeasurableSet s →
    ∀ (ht : MeasurableSet t),
      μ s ≠ ⊤ →
        ∀ (hμt : μ t ≠ ⊤) (x : G'),
          ∫ (a : α) in s, ↑↑(MeasureTheory.condExpIndSMul hm ht hμt x) a ∂μ = μ.real (t ∩ s) • x

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace