termVar[_|_] — Mathlib

English

Under SigmaFinite(μ.trim hm), Var[X; μ | m] equals a specified piecewise expression depending on integrability and measurability of the square difference.

Русский

При SigmaFinite(μ.trim hm) Var[X; μ | m] равно заданному кусочно-определённому выражению, зависящему от интегрируемости и измеримости квадратичного отклонения.

LaTeX

$$$ \text{[SigmaFinite]} \; Var[X; μ | m] = \begin{cases} \text{Integrable}((X-μ[X|m])^2) \rightarrow \text{ ... } \\ 0 \rightarrow \text{ ... } \end{cases} $$$

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₀`,
- `volume` is not σ-finite with respect to `m`,
- `X - 𝔼[X | m]` is not square-integrable. -/
@[scoped term_parser 1000]
public meta def «termVar[_|_]» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `ProbabilityTheory.«termVar[_|_]» 1024
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "Var[") (ParserDescr.cat✝ `term 0))
          (ParserDescr.symbol✝ "|"))
        (ParserDescr.cat✝ `term 0))
      (ParserDescr.symbol✝ "]"))

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