setLAverage_eq — Mathlib

English

On a set s, the laverage of f w.r.t. μ equals the integral of f over s divided by μ(s).

Русский

На множестве s среднее значение f по мере μ равно интегралу от f по s, делённому на μ(s).

LaTeX

$$$\\laverage_{\\mu}(f)\\text{ on } s = \\dfrac{\\int_{s} f \\, d\\mu}{\\mu(s)}$$$

Lean4

theorem setLAverage_eq (f : α → ℝ≥0∞) (s : Set α) : ⨍⁻ x in s, f x ∂μ = (∫⁻ x in s, f x ∂μ) / μ s := by
  rw [laverage_eq, restrict_apply_univ]

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