term⨍_In_,_∂_ — Mathlib

English

If μ is the zero measure, the average of any function is zero.

Русский

Если μ — нулевая мера, среднее любого функции равно 0.

LaTeX

$$$\\laverage_{0} f = 0$$$

Lean4

/-- Average value of a function `f` w.r.t. a measure `μ` on a set `s`.

It is equal to `(μ.real s)⁻¹ * ∫ x, f x ∂μ`, so it takes value zero if `f` is not integrable on
`s` or 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))

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