sigmaFinite_of_sigmaFiniteFiltration

English

If i ≤ j, and μ is sigma-finite on the j-th level, then the iterated conditional expectations satisfy the tower property: E[ E[g|ℱ_j] | ℱ_i ] = E[g|ℱ_i] a.e.

Русский

Если i ≤ j и μ ограничена на уровень ℱ_j, то тензорное ожидание выполняет правило башни: E[ E[g|ℱ_j] | ℱ_i ] = E[g|ℱ_i] почти наверно по μ.

LaTeX

$$$\\mu\\text{-a.e. }( \\mathbb E[ g|\\mathcal F_j]|\\mathcal F_i ) = \\mathbb E[ g|\\mathcal F_i]$, при $i\\le j$ и ${\\Sigma}$-finite условии.$$

Lean4

instance sigmaFinite_of_sigmaFiniteFiltration [Preorder ι] (μ : Measure Ω) (f : Filtration ι m)
    [hf : SigmaFiniteFiltration μ f] (i : ι) : SigmaFinite (μ.trim (f.le i)) :=
  hf.SigmaFinite _

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