condVar_of_sigmaFinite — Mathlib

English

If ΣFinite(μ.trim hm), condVar has a conditional-expression form that matches integrability and measurability assumptions.

Русский

Если ΣFinite(μ.trim hm), condVar имеет форму условного выражения, зависящего от интегрируемости и измеримости.

LaTeX

$$$ [SigmaFinite(μ.trim hm)] \Rightarrow Var[X; μ | m] = \text{condExp-form}(X, μ, m) $$$

Lean4

theorem condVar_of_sigmaFinite [SigmaFinite (μ.trim hm)] :
    Var[X; μ | m] =
      if Integrable (fun ω ↦ (X ω - (μ[X|m]) ω) ^ 2) μ then
        if StronglyMeasurable[m] (fun ω ↦ (X ω - (μ[X|m]) ω) ^ 2) then fun ω ↦ (X ω - (μ[X|m]) ω) ^ 2
        else aestronglyMeasurable_condExpL1.mk (condExpL1 hm μ fun ω ↦ (X ω - (μ[X|m]) ω) ^ 2)
      else 0 :=
  condExp_of_sigmaFinite _

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