English
For a real-valued density f, the measures μ.withDensity(ofReal f) and μ.withDensity(ofReal(-f)) are mutually singular.
Русский
Для вещественной плотности f меры μ.withDensity(ofReal f) и μ.withDensity(ofReal(-f)) взаимно седентарны (сепаратны).
LaTeX
$$ (μ.withDensity(ofReal f)) ⟂ μ.withDensity(ofReal(-f)) $$
Lean4
theorem withDensity_ofReal_mutuallySingular {f : α → ℝ} (hf : Measurable f) :
(μ.withDensity fun x => ENNReal.ofReal <| f x) ⟂ₘ μ.withDensity fun x => ENNReal.ofReal <| -f x :=
by
set S : Set α := {x | f x < 0}
have hS : MeasurableSet S := measurableSet_lt hf measurable_const
refine ⟨S, hS, ?_, ?_⟩
· rw [withDensity_apply _ hS, lintegral_eq_zero_iff hf.ennreal_ofReal, EventuallyEq]
exact (ae_restrict_mem hS).mono fun x hx => ENNReal.ofReal_eq_zero.2 (le_of_lt hx)
· rw [withDensity_apply _ hS.compl, lintegral_eq_zero_iff hf.neg.ennreal_ofReal, EventuallyEq]
exact (ae_restrict_mem hS.compl).mono fun x hx => ENNReal.ofReal_eq_zero.2 (not_lt.1 <| mt neg_pos.1 hx)
