withDensityᵥ_trim_eq_integral — Mathlib

English

For measurable i, the density-trim of μ.withDensityᵥ f over i equals the integral of f over i with respect to μ.

Русский

Для измеримого множества i плотностно-обрезанная мера μ.withDensityᵥ f над i равна интегралу f по i относительно μ.

LaTeX

$$$((\mu.withDensityᵥ f).trim hm) i = \int_{i} f \; d\mu$$$

Lean4

theorem withDensityᵥ_trim_eq_integral {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) {f : α → ℝ}
    (hf : Integrable f μ) {i : Set α} (hi : MeasurableSet[m] i) : (μ.withDensityᵥ f).trim hm i = ∫ x in i, f x ∂μ := by
  rw [VectorMeasure.trim_measurableSet_eq hm hi, withDensityᵥ_apply hf (hm _ hi)]

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