ae_withDensity_iff_ae_restrict — Mathlib

English

If f is measurable, the almost-everywhere statement under μ.withDensity f is equivalent to an ae-restrict statement under μ.

Русский

Если f измерима, то утверждение almost everywhere относительно μ.withDensity f эквивалентно ae-ограничению относительно μ.

LaTeX

$$$ (\\forall^\\infty x \\partial μ.withDensity f, p x) \\iff (\\forall^\\infty x \\partial μ, p x) $ при условии $f$ измерима$$

Lean4

theorem ae_withDensity_iff_ae_restrict {p : α → Prop} {f : α → ℝ≥0∞} (hf : Measurable f) :
    (∀ᵐ x ∂μ.withDensity f, p x) ↔ ∀ᵐ x ∂μ.restrict {x | f x ≠ 0}, p x :=
  ae_withDensity_iff_ae_restrict' <| hf.aemeasurable

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