ae_withDensity_iff' — Mathlib

English

For a density f, an almost-everywhere statement under μ.withDensity f is equivalent to an a.e. statement under μ with the hypothesis f ≠ 0.

Русский

Для плотности f равенство почти всюду при μ.withDensity f эквивалентно almost everywhere утверждению относительно μ с условием 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 : AEMeasurable f μ) :
    (∀ᵐ x ∂μ.withDensity f, p x) ↔ ∀ᵐ x ∂μ, f x ≠ 0 → p x :=
  by
  rw [ae_iff, ae_iff, withDensity_apply_eq_zero' hf, iff_iff_eq]
  congr
  ext x
  simp only [exists_prop, mem_inter_iff, mem_setOf_eq, not_forall]

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