term__[|_←_] — Mathlib

English

If X is scaled by c, the conditional variance scales by c^2 a.e.

Русский

Если X масштабируется на c, условная дисперсия пропорциональна c^2 почти наверняка.

LaTeX

$$$\\mathrm{Var}[c \\cdot X; μ | m] =^a.e_ μ \\; c^2 \\cdot \\mathrm{Var}[X; μ | m]$$$

Lean4

/-- The conditional probability measure of measure `μ` on `{ω | X ω = x}`.

It is `μ` restricted to `{ω | X ω = x}` and scaled by the inverse of `μ {ω | X ω = x}`
(to make it a probability measure): `(μ {ω | X ω = x})⁻¹ • μ.restrict {ω | X ω = x}`. -/
@[scoped term_parser 1000]
public meta def «term__[|_←_]» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `ProbabilityTheory.«term__[|_←_]» 1024 0
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.unary✝ `group (ParserDescr.const✝ `noWs))
              (ParserDescr.symbol✝ "[|"))
            (ParserDescr.cat✝ `term 0))
          (ParserDescr.symbol✝ " ← "))
        (ParserDescr.cat✝ `term 0))
      (ParserDescr.symbol✝ "]"))

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