aemeasurable_withDensity_ennreal_iff

English

If f is measurable, there is an equivalence between AEMeasurability with density and a density-scaled AEMeasurability for ENNReal values.

Русский

Если f измерима, существует эквивалентность между AЕМас measurable с плотностью и AЕМас измеримостью после масштабирования ENNReal.

LaTeX

$$AEMeasurable g (μ.withDensity (f : ENNReal)) ↔ AEMeasurable ((f : ENNReal) * g) μ$$

Lean4

theorem aemeasurable_withDensity_ennreal_iff {f : α → ℝ≥0} (hf : Measurable f) {g : α → ℝ≥0∞} :
    AEMeasurable g (μ.withDensity fun x => (f x : ℝ≥0∞)) ↔ AEMeasurable (fun x => (f x : ℝ≥0∞) * g x) μ :=
  aemeasurable_withDensity_ennreal_iff' <| hf.aemeasurable

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