English
A version of the previous lemma with simplification.
Русский
Версия предыдущего лема с упрощением.
LaTeX
$$$\\operatorname{condVar\\_smul}(c,X)\\; :\\; \\mathrm{Var}[c \\cdot X; μ | m] =^a.e_ μ c^2 \\cdot \\mathrm{Var}[X; μ | m]$$$
Lean4
/-- The conditional probability measure of measure `μ` on set `{ω | 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.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✝ " ← "))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ "]"))
