setIntegral_condVar — Mathlib

English

Var[X; μ | m] is strongly measurable with respect to m.

Русский

Var[X; μ | m] является сильно измеримой по отношению к m.

LaTeX

$$$ StronglyMeasurable_m( Var[X; μ | m] ) $$$

Lean4

/-- 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. -/
theorem setIntegral_condVar [SigmaFinite (μ.trim hm)] (hX : Integrable ((X - μ[X|m]) ^ 2) μ) (hs : MeasurableSet[m] s) :
    ∫ ω in s, (Var[X; μ | m]) ω ∂μ = ∫ ω in s, (X ω - (μ[X|m]) ω) ^ 2 ∂μ :=
  setIntegral_condExp _ hX hs

Похожие утверждения