term__[_] — Mathlib

English

Var(X) ≤ (b−a)^2/4 when a ≤ X ≤ b a.e. under a probability measure.

Русский

Если X лежит в интервале [a,b] почти surely, то Var(X) ≤ (b−a)^2/4.

LaTeX

$$$\operatorname{Var}[X;\, \mu] \le \left(\frac{b-a}{2}\right)^2$$

Lean4

/-- `P[X]` is the expectation of `X` under the measure `P`.

Note that this notation can conflict with the `GetElem` notation for lists. Usually if you see an
error about ambiguous notation when trying to write `l[i]` for a list, it means that Lean could
not find `i < l.length`, and so fell back to trying this notation as well. -/
@[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.unary✝ `group (ParserDescr.const✝ `noWs)) (ParserDescr.symbol✝ "["))
        (ParserDescr.cat✝ `term 0))
      (ParserDescr.symbol✝ "]"))

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