condExp_condExp — Mathlib

English

For a function f, filtration ℱ, and i ≤ j, the double conditional expectation equals the single one almost everywhere under sigma-finiteness assumptions.

Русский

Для функции f, фильтрации ℱ и i ≤ j, двойное условное ожидание ≡ единичному почти повсеместно при условии сигма‑финитности.

LaTeX

$$$\\forall i\\le j,\\; [\\SigmaFinite (μ.trim (ℱ.le j))] \\Rightarrow μ[ μ[f|ℱ j]|ℱ i] =^{a.e.}_{μ} μ[f|ℱ i]$$$

Lean4

theorem condExp_condExp [Preorder ι] {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : Ω → E)
    {μ : Measure Ω} (ℱ : Filtration ι m) {i j : ι} (hij : i ≤ j) [SigmaFinite (μ.trim (ℱ.le j))] :
    μ[μ[f|ℱ j]|ℱ i] =ᵐ[μ] μ[f|ℱ i] :=
  condExp_condExp_of_le (ℱ.mono hij) (ℱ.le j)

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