Theorems · Theorem · measure theory

MeasureTheory.condExp_def

∀ {α : Type u_5} {E : Type u_6} (m : MeasurableSpace α) {m₀ : MeasurableSpace α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] (μ : MeasureTheory.Measure α) (f : α → E),
  μ[f | m] =
    if hm : m ≤ m₀ then
      if h : MeasureTheory.SigmaFinite (μ.trim hm) ∧ MeasureTheory.Integrable f μ then
        if MeasureTheory.StronglyMeasurable f then f
        else
          have this := ⋯;
          MeasureTheory.AEStronglyMeasurable.mk ↑↑(MeasureTheory.condExpL1 hm μ f) ⋯
      else 0
    else 0

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace