Theorems · Theorem · measure theory

MeasureTheory.condExp_bilin_of_stronglyMeasurable_left

∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} {F : Type u_3} {G : Type u_4}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] [CompleteSpace G] (B : F →L[ℝ] E →L[ℝ] G) [CompleteSpace E]
  {f : Ω → F} {g : Ω → E},
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.Integrable (fun ω => (B (f ω)) (g ω)) μ →
      MeasureTheory.Integrable g μ → μ[fun ω => (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω => (B (f ω)) (μ[g | m] ω)

Pull-out property of the conditional expectation.

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceCompleteSpaceCompleteSpace