trim_withDensity — Mathlib

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)]

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