Theorems · Theorem · probability

ProbabilityTheory.condVar_of_sigmaFinite

∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {hm : m ≤ m₀} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [inst : MeasureTheory.SigmaFinite (μ.trim hm)],
  ProbabilityTheory.condVar m X μ =
    if MeasureTheory.Integrable (fun ω => (X ω - μ[X | m] ω) ^ 2) μ then
      if MeasureTheory.StronglyMeasurable fun ω => (X ω - μ[X | m] ω) ^ 2 then fun ω => (X ω - μ[X | m] ω) ^ 2
      else MeasureTheory.AEStronglyMeasurable.mk ↑↑(MeasureTheory.condExpL1 hm μ fun ω => (X ω - μ[X | m] ω) ^ 2) ⋯
    else 0

Defined in

Mathlib.Probability.CondVar

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SigmaFinite