Theorems · Theorem · measure theory

ContinuousLinearMap.comp_condExp_add_const_comm

∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {F : Type u_5}
  [inst_3 : NormedAddCommGroup F] [CompleteSpace F] [inst_5 : NormedSpace ℝ F] [MeasureTheory.IsFiniteMeasure μ],
  m ≤ m₀ →
    MeasureTheory.Integrable f μ →
      ∀ (T : E →L[ℝ] F) (a : F), (fun x => T (μ[f | m] x) + a) =ᵐ[μ] μ[fun y => T (f y) + a | m]

Conditional expectation commutes with affine functions. Note that IsFiniteMeasure μ is a necessary assumption because we want constant functions to be integrable.

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceNormedAddCommGroupCompleteSpaceNormedSpaceMeasureTheory.IsFiniteMeasure