condVar — Mathlib

English

The conditional variance Var[X; μ | m] is defined as μ[(X − μ[X|m])^2|m].

Русский

Условная дисперсия Var[X; μ | m] определяется как μ[(X − μ[X|m])^2|m].

LaTeX

$$$ \mathrm{condVar}(X; \mu | m) = \mu[(X - \mu[X|m])^2 | m] $$$

Lean4

/-- Conditional variance of a real-valued random variable. It is defined as `0` if any one of the
following conditions is true:
- `m` is not a sub-σ-algebra of `m₀`,
- `μ` is not σ-finite with respect to `m`,
- `X - μ[X | m]` is not square-integrable. -/
noncomputable def condVar : Ω → ℝ :=
  μ[(X - μ[X|m]) ^ 2|m]

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