termEVar[_;_] — Mathlib

English

The variance of X under the tilted measure equals the second derivative of cg f at t, provided ht holds.

Русский

Дисперсия X при смещённой мере равна второй производной cg f в точке t при условии ht.

LaTeX

$$$\\operatorname{Var}[X; μ_{tX}] = \\operatorname{iteratedDeriv}_{2}(\\operatorname{cgf}(X, μ), t)$$$

Lean4

/-- The `ℝ≥0∞`-valued variance of the real-valued random variable `X` according to the measure `μ`.

This is defined as the Lebesgue integral of `(X - 𝔼[X])^2`. -/
@[scoped term_parser 1000]
public meta def «termEVar[_;_]» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `ProbabilityTheory.«termEVar[_;_]» 1024
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "eVar[") (ParserDescr.cat✝ `term 0))
          (ParserDescr.symbol✝ "; "))
        (ParserDescr.cat✝ `term 0))
      (ParserDescr.symbol✝ "]"))

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