term⨍_,_∂_ — Mathlib

English

The laverage of a constant function equals the constant, consistent with previous theorems.

Русский

Среднее константы равно самой константе.

LaTeX

$$$\\laverage_{μ} (c) = c$$$

Lean4

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

It is equal to `(μ.real univ)⁻¹ • ∫ x, f x ∂μ`, so it takes value zero if `f` is not integrable or
if `μ` is an infinite measure. If `μ` is a probability measure, then the average of any function is
equal to its integral.

For the average on a set, use `⨍ x in s, f x ∂μ`, defined as `⨍ x, f x ∂(μ.restrict s)`. For the
average w.r.t. the volume, one can omit `∂volume`. -/
@[term_parser 1000]
public meta def «term⨍_,_∂_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `MeasureTheory.«term⨍_,_∂_» 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "⨍") Batteries.ExtendedBinder.extBinders)
            (ParserDescr.symbol✝ ", "))
          (ParserDescr.cat✝ `term 60))
        (ParserDescr.symbol✝ " ∂"))
      (ParserDescr.cat✝ `term 70))

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