variance — Mathlib

English

The variance of X under the tilted measure μ.tilted(tX) equals the second derivative of the cumulant generating function cg f at t.

Русский

Дисперсию X по смещённой мере μ_tilted(tX) можно выразить как вторую производную cg f в точке t.

LaTeX

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

Lean4

/-- The `ℝ`-valued variance of a real-valued random variable defined by applying `ENNReal.toReal`
to `evariance`. -/
def variance : ℝ :=
  (evariance X μ).toReal

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