English
Properties of laverage with constants across restrictions and measures.
Русский
Свойства лаverage констант относительно ограничений и мер.
LaTeX
$$$\\laverage_{μ|s}(c) = c$ при подходящих условиях; $\\laverage_{μ}(c) = c$$$
Lean4
/-- Average value of a function `f` w.r.t. the standard measure.
It is equal to `(volume.real univ)⁻¹ * ∫ x, f x`, so it takes value zero if `f` is not integrable
or if the space has infinite measure. In a probability space, 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 ∂(volume.restrict s)`. -/
@[term_parser 1000]
public meta def «term⨍_,_» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `MeasureTheory.«term⨍_,_» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "⨍") Batteries.ExtendedBinder.extBinders)
(ParserDescr.symbol✝ ", "))
(ParserDescr.cat✝ `term 60))
