English
For any μ on α and any real-valued density f: α → ℝ, the vector measure μ.withDensityᵥ f is absolutely continuous with respect to μ.toENNRealVectorMeasure; if f is integrable then stronger absolute continuity holds for the trimmed measure as well.
Русский
Для любой меры μ на α и плотности f: α → ℝ плотностная векторная мера μ.withDensityᵥ f относительно μ.toENNRealVectorMeasure; если f интегрируемо, то аналогично существует более сильная абсолютная непрерывность для обрезанной меры.
LaTeX
$$$\mu.withDensityᵥ f \ll^{\vee} \mu^{\mathrm{toENNRealVectorMeasure}}$$
Lean4
theorem withDensityᵥ_absolutelyContinuous (μ : Measure α) (f : α → ℝ) : μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure :=
by
by_cases hf : Integrable f μ
· refine VectorMeasure.AbsolutelyContinuous.mk fun i hi₁ hi₂ => ?_
rw [toENNRealVectorMeasure_apply_measurable hi₁] at hi₂
rw [withDensityᵥ_apply hf hi₁, Measure.restrict_zero_set hi₂, integral_zero_measure]
· rw [withDensityᵥ, dif_neg hf]
exact VectorMeasure.AbsolutelyContinuous.zero _
