English
For any function f: X → ℝ≥0∞, the left average with respect to μ equals the scaled integral (definition of laverage).
Русский
Для любой функции f: X → ℝ≥0∞ левое среднее по отношению к μ равно масштабируемому интегралу (определение laverage).
LaTeX
$$$\\mathrm{laverage}(f) \\;=\\; \\mathrm{lintegral}(f)\\ \\, \\text{with appropriate scaling}$$$
Lean4
/-- Average value of an `ℝ≥0∞`-valued function `f` w.r.t. the standard measure.
It is equal to `(volume univ)⁻¹ * ∫⁻ x, f x`, so it takes value zero 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))
