Integral average of a function #
In this file we define measure_theory.average μ f
(notation: ⨍ x, f x ∂μ
) to be the average
value of f
with respect to measure μ
. It is defined as ∫ x, f x ∂((μ univ)⁻¹ • μ)
, so it
is equal to 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, we use ⨍ x in s, f x ∂μ
(notation for ⨍ x, f x ∂(μ.restrict s)
). For
average w.r.t. the volume, one can omit ∂volume
.
Implementation notes #
The average is defined as an integral over (μ univ)⁻¹ • μ
so that all theorems about Bochner
integrals work for the average without modifications. For theorems that require integrability of a
function, we provide a convenience lemma measure_theory.integrable.to_average
.
Tags #
integral, center mass, average value
Average value of a function w.r.t. a measure #
The average value of a function f
w.r.t. a measure μ
(notation: ⨍ x, f x ∂μ
) is defined as
(μ univ).to_real⁻¹ • ∫ x, f x ∂μ
, so it is equal to 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.
Average value of a function f
w.r.t. a measure μ
, notation: ⨍ x, f x ∂μ
. It is defined as
(μ univ).to_real⁻¹ • ∫ x, f x ∂μ
, so it is equal to 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
average w.r.t. the volume, one can omit ∂volume
.