measurableSet_of_filtration — Mathlib

English

Let g be integrable with respect to μ. Then the family of conditional expectations E[g|f_i] is uniformly integrable in L^1(μ) with respect to the filtration (f_i).

Русский

Пусть g интегрируемо по μ. Тогда семейство условных математических ожиданий E[g|ℱ_i] является равномерно интегрируемым в L^1(μ) по фильтрации (ℱ_i).

LaTeX

$$$\\text{Integrable } g,\\; \\{ \\mathbb E[g|\\mathcal F_i] : i \\in ι\\} \\text{ is UniformIntegrable in } L^1(μ).$$$

Lean4

theorem measurableSet_of_filtration [Preorder ι] {f : Filtration ι m} {s : Set Ω} {i : ι} (hs : MeasurableSet[f i] s) :
    MeasurableSet[m] s :=
  f.le i s hs

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