term⨍⁻_In_,_ — Mathlib

English

Reiterates that for a probability measure μ, the left average of f equals the integral of f with respect to μ.

Русский

Повторение: для вероятностной меры μ левое среднее f совпадает с интегралом по μ.

LaTeX

$$$\\mathrm{laverage}(μ, f) = \\int f \\, dμ$$$

Lean4

/-- Average value of an `ℝ≥0∞`-valued function `f` w.r.t. the standard measure on a set `s`.

It is equal to `(volume s)⁻¹ * ∫⁻ x, f x`, so it takes value zero if `s` has infinite measure. If
`s` has measure `1`, then the average of any function is equal to its integral. -/
@[term_parser 1000]
public meta def «term⨍⁻_In_,_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `MeasureTheory.«term⨍⁻_In_,_» 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "⨍⁻") Batteries.ExtendedBinder.extBinders)
            (ParserDescr.symbol✝ " in "))
          (ParserDescr.cat✝ `term 0))
        (ParserDescr.symbol✝ ", "))
      (ParserDescr.cat✝ `term 60))

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