uniformIntegrable_condExp_filtration

English

If g is integrable w.r.t. μ, then the conditional expectations with respect to the filtration are uniformly integrable; this is a refinement of 172080 with more general indexing.

Русский

Если g интегрируемо по μ, то условные ожидания относительно фильтрации единообразно интегрируемы; более широкий вариант 172080.

LaTeX

$$$\\forall i,\\; U I ( E[g|F_i] )_{i} \\text{ is UniformIntegrable}$$$

Lean4

/-- Given an integrable function `g`, the conditional expectations of `g` with respect to a
filtration is uniformly integrable. -/
theorem uniformIntegrable_condExp_filtration [Preorder ι] {μ : Measure Ω} [IsFiniteMeasure μ] {f : Filtration ι m}
    {g : Ω → ℝ} (hg : Integrable g μ) : UniformIntegrable (fun i => μ[g|f i]) 1 μ :=
  hg.uniformIntegrable_condExp f.le

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