measure_compl_aeSeqSet_eq_zero — Mathlib

English

If all f i are AEMeasurable and p(x,f) holds almost everywhere, the complement of aeSeqSet hf p has μ-measure zero.

Русский

Если все f i являются AEMeasurable и p(x,f) выполняется почти всюду, дополнение aeSeqSet hf p имеет нулевую меру μ.

LaTeX

$$$ \mu\big((aeSeqSet\, hf\, p)^{c}\big) = 0 $$$

Lean4

theorem measure_compl_aeSeqSet_eq_zero [Countable ι] (hf : ∀ i, AEMeasurable (f i) μ)
    (hp : ∀ᵐ x ∂μ, p x fun n => f n x) : μ (aeSeqSet hf p)ᶜ = 0 :=
  by
  rw [aeSeqSet, compl_compl, measure_toMeasurable]
  have hf_eq := fun i => (hf i).ae_eq_mk
  simp_rw [Filter.EventuallyEq, ← ae_all_iff] at hf_eq
  exact Filter.Eventually.and hf_eq hp

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