English
If f is locally integrable, ‖f(−x)‖ = ‖f(x)‖ a.e., and f = O[atTop] g with g integrable atTop, then f is integrable.
Русский
Если f локально интегрируема, почти везде выполнено равенство норм, и f = O[atTop] g с g интегрируемой, тогда f интегрируемо.
LaTeX
$$$\\mathrm{Integrable}\\ f$ under given BigO and symmetry$$
Lean4
/-- Average value of an `ℝ≥0∞`-valued function `f` w.r.t. a measure `μ`, denoted `⨍⁻ x, f x ∂μ`.
It is equal to `(μ univ)⁻¹ * ∫⁻ x, f x ∂μ`, so it takes value zero 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 laverage (f : α → ℝ≥0∞) :=
∫⁻ x, f x ∂(μ univ)⁻¹ • μ
