aeSeq_eq_mk_ae — Mathlib

English

There exists a set of full μ-measure on which for every i we have aeSeq hf p i a = (hf i).mk (f i) a.

Русский

Существует множество полного μ-измерения, на котором для каждого i выполняется aeSeq hf p i a = (hf i).mk (f i) a.

LaTeX

$$$ \forall^* a \partial\mu,\ \forall i,\ aeSeq\, hf\, p\, i\, a = (hf i).mk\,(f i)\, a $$$

Lean4

theorem aeSeq_eq_mk_ae [Countable ι] (hf : ∀ i, AEMeasurable (f i) μ) (hp : ∀ᵐ x ∂μ, p x fun n => f n x) :
    ∀ᵐ a : α ∂μ, ∀ i : ι, aeSeq hf p i a = (hf i).mk (f i) a :=
  have h_ss : aeSeqSet hf p ⊆ {a : α | ∀ i, aeSeq hf p i a = (hf i).mk (f i) a} := fun x hx i => by
    simp only [aeSeq, hx, if_true]
  (ae_iff.2 (measure_compl_aeSeqSet_eq_zero hf hp)).mono h_ss

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