English
If f is a.e. positive, then μ ≪ μ.withDensity f; i.e., μ is absolutely continuous with respect to the density-modified measure.
Русский
Если почти всюду положительно, то μ абсолютно непрерывна относительно μ.withDensity f.
LaTeX
$$μ ≪ μ.withDensity f$$
Lean4
/-- If `f` is almost everywhere positive, then `μ ≪ μ.withDensity f`. See also
`withDensity_absolutelyContinuous` for the reverse direction, which always holds. -/
theorem withDensity_absolutelyContinuous' {μ : Measure α} {f : α → ℝ≥0∞} (hf : AEMeasurable f μ)
(hf_ne_zero : ∀ᵐ x ∂μ, f x ≠ 0) : μ ≪ μ.withDensity f :=
by
refine Measure.AbsolutelyContinuous.mk (fun s hs hμs ↦ ?_)
rw [withDensity_apply _ hs, lintegral_eq_zero_iff' hf.restrict, ae_eq_restrict_iff_indicator_ae_eq hs,
Set.indicator_zero', Filter.EventuallyEq, ae_iff] at hμs
simp only [ae_iff, ne_eq, not_not] at hf_ne_zero
simp only [Pi.zero_apply, Set.indicator_apply_eq_zero, not_forall, exists_prop] at hμs
have hle : s ⊆ {a | a ∈ s ∧ ¬f a = 0} ∪ {a | f a = 0} := fun x hx ↦ or_iff_not_imp_right.mpr <| fun hnx ↦ ⟨hx, hnx⟩
exact
measure_mono_null hle <|
nonpos_iff_eq_zero.1 <| le_trans (measure_union_le _ _) <| hμs.symm ▸ zero_add _ |>.symm ▸ hf_ne_zero.le
