English
If μ is sigma-finite, then μ.rnDer ν is almost everywhere finite with respect to ν.
Русский
Если μ слабосчитаема, то μ.rnDer ν конечен почти всюду по ν.
LaTeX
$$$\\text{If } μ \\text{ is sigma-finite, then } μ\\mathrm{rnDer}\\nu <_∞ ν\\text{-ae}$$$
Lean4
/-- The Radon-Nikodym derivative of a sigma-finite measure `μ` with respect to another
measure `ν` is `ν`-almost everywhere finite. -/
theorem rnDeriv_lt_top (μ ν : Measure α) [SigmaFinite μ] : ∀ᵐ x ∂ν, μ.rnDeriv ν x < ∞ :=
by
suffices ∀ n, ∀ᵐ x ∂ν, x ∈ spanningSets μ n → μ.rnDeriv ν x < ∞ by
filter_upwards [ae_all_iff.2 this] with _ hx using hx _ (mem_spanningSetsIndex _ _)
intro n
rw [← ae_restrict_iff' (measurableSet_spanningSets _ _)]
apply ae_lt_top (measurable_rnDeriv _ _)
refine (lintegral_rnDeriv_lt_top_of_measure_ne_top _ ?_).ne
exact (measure_spanningSets_lt_top _ _).ne
