withDensity_indicator — Mathlib

English

The density with an indicator of a measurable set s satisfies μ.withDensity(s.indicator f) = (μ.restrict s).withDensity f.

Русский

Плотность с индикацией множества s удовлетворяет равенству μ.withDensity(s.indicator f) = (μ.restrict s).withDensity f.

LaTeX

$$$\\mu.withDensity(s.indicator f) = (\\mu\\restriction s).withDensity f$$$

Lean4

theorem withDensity_indicator {s : Set α} (hs : MeasurableSet s) (f : α → ℝ≥0∞) :
    μ.withDensity (s.indicator f) = (μ.restrict s).withDensity f :=
  by
  ext1 t ht
  rw [withDensity_apply _ ht, lintegral_indicator hs, restrict_comm hs, ← withDensity_apply _ ht]

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