ae_withDensity_iff — Mathlib

English

If f is measurable, the ae-implication under μ.withDensity f is equivalent to an ae-implication under μ with the a.e. condition f ≠ 0.

Русский

Если f измерима, то эквивалентность Almost Everywhere утверждений между μ.withDensity f и μ сохраняется при условии f ≠ 0.

LaTeX

$$$(\\forall^\\infty x \\partial μ.withDensity f, p x) \\iff (\\forall^\\infty x \\partial μ, f x \\neq 0 \\to p x)$$$

Lean4

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

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