Theorems · Theorem · probability

ProbabilityTheory.setIntegral_condVar

∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {hm : m ≤ m₀} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {s : Set Ω}
  [MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasureTheory.Integrable ((X - μ[X | m]) ^ 2) μ →
    MeasurableSet s → ∫ (ω : Ω) in s, ProbabilityTheory.condVar m X μ ω ∂μ = ∫ (ω : Ω) in s, (X ω - μ[X | m] ω) ^ 2 ∂μ

The integral of the conditional variance Var[X | m] over an m-measurable set is equal to the integral of (X - μ[X | m]) ^ 2 on that set.

Defined in

Mathlib.Probability.CondVar

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SigmaFinite