English
Trimming the measure after density equals applying density after trimming the measure.
Русский
Обрезка меры после плотности равна применению плотности после обрезки меры.
LaTeX
$$(\\mu.withDensity f).trim hm = (\\mu.trim hm).withDensity f$$
Lean4
theorem trim_withDensity {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) {f : α → ℝ≥0∞}
(hf : Measurable[m] f) : (μ.withDensity f).trim hm = (μ.trim hm).withDensity f :=
by
refine @Measure.ext _ m _ _ (fun s hs ↦ ?_)
rw [withDensity_apply _ hs, restrict_trim _ _ hs, lintegral_trim _ hf, trim_measurableSet_eq _ hs,
withDensity_apply _ (hm s hs)]