condVar_of_aestronglyMeasurable — Mathlib

English

Under AEStronglyMeasurable X, condVar equals a.e. (X − μ[X|m])^2 if integrable.

Русский

При AEStronglyMeasurable X condVar равен a.e. (X − μ[X|m])^2 при интегрируемости.

LaTeX

$$$ (\text{ae})\; Var[X; μ | m] = (X - μ[X|m])^2 \text{ a.e.} $$$

Lean4

theorem condVar_of_aestronglyMeasurable [hμm : SigmaFinite (μ.trim hm)] (hX : AEStronglyMeasurable[m] X μ)
    (hXint : Integrable ((X - μ[X|m]) ^ 2) μ) : Var[X; μ | m] =ᵐ[μ] (X - μ[X|m]) ^ 2 :=
  condExp_of_aestronglyMeasurable' _
    ((continuous_pow _).comp_aestronglyMeasurable (hX.sub stronglyMeasurable_condExp.aestronglyMeasurable)) hXint

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