Theorems · Theorem · probability

ProbabilityTheory.condVar_of_aestronglyMeasurable

∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {hm : m ≤ m₀} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [hμm : MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasureTheory.AEStronglyMeasurable X μ →
    MeasureTheory.Integrable ((X - μ[X | m]) ^ 2) μ → ProbabilityTheory.condVar m X μ =ᵐ[μ] (X - μ[X | m]) ^ 2

Defined in

Mathlib.Probability.CondVar

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SigmaFinite