English
For locally finite μ, absolutely continuous ρ ≪ μ, the ratio ρ a / μ a tends to the measurable limRatioMeas hρ almost everywhere along the Vitali filter.
Русский
Для локально конечной меры μ и ρ ≪ μ отношение ρ(a)/μ(a) стремится к измеримому limRatioMeas hρ почти везде вдоль фильтра Vitali.
LaTeX
$$$\forall x,\ Tendsto (a\mapsto ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x)).$$$
Lean4
theorem aemeasurable_limRatio : AEMeasurable (v.limRatio ρ) μ :=
by
apply ENNReal.aemeasurable_of_exist_almost_disjoint_supersets _ _ fun p q hpq => ?_
exact v.exists_measurable_supersets_limRatio hρ hpq