English
Let μ and ν be measures with μ absolutely continuous with respect to ν and with μ σ-finite. If ν admits a Lebesgue decomposition with respect to μ, then the Radon–Nikodym derivative dμ/dν is strictly positive μ-a.e.
Русский
Пусть μ и ν — меры, причём μ абсолютно непрерывна по ν, и μ счётно конечна. Если ν имеет разложение Лебега относительно μ, то производная Радона–Никодима dμ/dν положительна μ-почти всюду.
LaTeX
$$$(\\nu.rnDeriv \\mu)(x) > 0\\quad\\text{для μ-λ. д. x}$$$
Lean4
theorem rnDeriv_pos' [HaveLebesgueDecomposition ν μ] [SigmaFinite μ] (hμν : μ ≪ ν) : ∀ᵐ x ∂μ, 0 < ν.rnDeriv μ x :=
by
refine (absolutelyContinuous_withDensity_rnDeriv hμν).ae_le ?_
filter_upwards [Measure.rnDeriv_pos (withDensity_absolutelyContinuous μ (ν.rnDeriv μ)),
(withDensity_absolutelyContinuous μ (ν.rnDeriv μ)).ae_le
(Measure.rnDeriv_withDensity μ (Measure.measurable_rnDeriv ν μ))] with
x hx hx2
rwa [← hx2]
