English
Constant f yields constant laverage on s under appropriate μ(s).
Русский
Для константы f среднее по любому допустимому s равно константе.
LaTeX
$$$\\laverage_{μ|s}(c) = c$ при $μ(s) ≠ 0$ и $μ(s) ≠ ∞$$$
Lean4
/-- Average value of a function `f` w.r.t. a measure `μ`, denoted `⨍ x, f x ∂μ`.
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`. -/
noncomputable def average (f : α → E) :=
∫ x, f x ∂(μ univ)⁻¹ • μ
