withDensityᵥ_trim_absolutelyContinuous

English

For any measurable hm, the trimmed density μ.withDensityᵥ f is absolutely continuous with respect to the trimmed ENNReal-vector measure of μ.

Русский

Для любой выпуклости измеримости hm обрезанная плотность μ.withDensityᵥ f абсолютно непрерывна по отношению к обрезанной ENNReal-векторной мере μ.

LaTeX

$$$(\mu.withDensityᵥ f).trim hm \ll^{\vee} (\mu.trim hm).toENNRealVectorMeasure$$

Lean4

theorem withDensityᵥ_trim_absolutelyContinuous {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0)
    (hfi : Integrable f μ) : (μ.withDensityᵥ f).trim hm ≪ᵥ (μ.trim hm).toENNRealVectorMeasure :=
  by
  refine VectorMeasure.AbsolutelyContinuous.mk fun j hj₁ hj₂ => ?_
  rw [Measure.toENNRealVectorMeasure_apply_measurable hj₁, trim_measurableSet_eq hm hj₁] at hj₂
  rw [VectorMeasure.trim_measurableSet_eq hm hj₁, withDensityᵥ_apply hfi (hm _ hj₁)]
  simp only [Measure.restrict_eq_zero.mpr hj₂, integral_zero_measure]

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