integral_average — Mathlib

English

The average of f over μ equals the integral of f divided by μ(univ); the integral of the averaged function equals the original integral scaled by μ(univ).

Русский

Среднее по μ равно интегралу от f, делённому на μ(univ); интеграл по усреднённой функции равен исходному интегралу, делённому на μ(univ).

LaTeX

$$$\int_\alpha f \, d\mu = μ(\mathrm{univ}) \cdot \operatorname{average}_\mu f$$$

Lean4

theorem integral_average (μ : Measure α) [IsFiniteMeasure μ] (f : α → E) : ∫ _, ⨍ a, f a ∂μ ∂μ = ∫ x, f x ∂μ := by simp

Похожие утверждения