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]