aemeasurable_limRatio — Mathlib

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

Похожие утверждения