termEVar[_] — Mathlib

English

If evariance is finite, it is < ∞; otherwise it equals ∞.

Русский

Если evariance конечна, она меньше чем бесконечность; иначе равна бесконечности.

LaTeX

$$evariance X μ < ∞ ↔ MemLp X 2 μ$$

Lean4

/-- The `ℝ≥0∞`-valued variance of the real-valued random variable `X` according to the volume
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.symbol✝ "eVar[") (ParserDescr.cat✝ `term 0)) (ParserDescr.symbol✝ "]"))

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