term⨍⁻_In_,_∂_ — Mathlib

English

If μ is a probability measure, the left average equals the ordinary integral of f with respect to μ.

Русский

Если μ — вероятностная мера, левое среднее равно обычному интегралу функции f по μ.

LaTeX

$$$\\mathrm{laverage}\\;μ\\;f = \\mathrm{lintegral}\\;μ\\; f$$$

Lean4

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

It is equal to `(μ 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.

For the average w.r.t. the volume, one can omit `∂volume`. -/
@[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.binary✝ `andthen
                (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "⨍⁻") Batteries.ExtendedBinder.extBinders)
                (ParserDescr.symbol✝ " in "))
              (ParserDescr.cat✝ `term 0))
            (ParserDescr.symbol✝ ", "))
          (ParserDescr.cat✝ `term 60))
        (ParserDescr.symbol✝ " ∂"))
      (ParserDescr.cat✝ `term 70))

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