Theorems · Theorem · measure theory

MeasureTheory.condExp_mul_of_aestronglyMeasurable_right

∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f g : Ω → ℝ},
  MeasureTheory.AEStronglyMeasurable g μ →
    MeasureTheory.Integrable (f * g) μ → MeasureTheory.Integrable f μ → μ[f * g | m] =ᵐ[μ] μ[f | m] * g

Pull-out property of the conditional expectation.

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Cited by

0 results in Mathlib

Foundations

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