withDensity_apply — Mathlib

English

For measurable s, the measure of s under μ with density f equals the integral of f over s with respect to μ.

Русский

Для измеримого множества s значение меры μ с плотностью f на s равно интегралу f по μ на s.

LaTeX

$$$(\mu\text{ withDensity } f)(s) = \int_{s} f \, d\mu$$$

Lean4

@[simp]
theorem withDensity_apply (f : α → ℝ≥0∞) {s : Set α} (hs : MeasurableSet s) : μ.withDensity f s = ∫⁻ a in s, f a ∂μ :=
  Measure.ofMeasurable_apply s hs

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