English
If μ is a nonzero finite measure and f: Ω → E (E a NormedSpace), then the average with respect to μ equals the integral of f against μ normalized.
Русский
Пусть μ — ненулевая конечная мера и f: Ω → E (E — нормированное пространство). Тогда среднее по μ равно интегралу f по нормированной мере μ.
LaTeX
$$$\\forall E\\text{ } [\\_normalsymbol E], (nonzero : μ \\neq 0) \\Rightarrow \\operatorname{average}(μ: \\ Measure Ω) f = \\int_Ω f(ω)\\, d(μ.\\mathrm{normalize}: \\ Measure Ω).$$$
Lean4
/-- Averaging with respect to a finite measure is the same as integrating against
`MeasureTheory.FiniteMeasure.normalize`. -/
theorem average_eq_integral_normalize {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (nonzero : μ ≠ 0)
(f : Ω → E) : average (μ : Measure Ω) f = ∫ ω, f ω ∂(μ.normalize : Measure Ω) :=
by
rw [μ.toMeasure_normalize_eq_of_nonzero nonzero, average]
congr
simp [ENNReal.coe_inv (μ.mass_nonzero_iff.mpr nonzero), ennreal_mass]
