term⨍_In_,_ — Mathlib

English

Introductory note about the average definition and basic properties.

Русский

Вводная заметка о определении среднего и базовых свойствах.

LaTeX

$$$\\text{average}(f) := ∫ f dμ \\;/\\; μ(\\mathrm{univ})$$$

Lean4

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

It is equal to `(volume.real s)⁻¹ * ∫ x, f x`, so it takes value zero `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. -/
@[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))

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