Theorems · Theorem · measure theory

MeasureTheory.condExp_add

∀ {α : Type u_1} {E : Type u_3} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E],
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ → ∀ (m : MeasurableSpace α), μ[f + g | m] =ᵐ[μ] μ[f | m] + μ[g | m]

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Cited by

11 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace