condExp_ae_le — Mathlib

English

If f is a supermartingale, then for all i ≤ j the conditional expectation μ[f_j | ℱ_i] is almost surely less than or equal to f_i.

Русский

Если f — суперmartingale, то для любых i ≤ j условное ожидание μ[f_j | ℱ_i] почти наверняка не превосходит f_i.

LaTeX

$$$\mathrm{Submartingale}(f,\mathcal{F},\mu) \Rightarrow \forall i,j,\ i \le j \Rightarrow \mu[f_j|\mathcal{F}_i] \le_{a.e.} f_i$$$

Lean4

theorem condExp_ae_le [LE E] (hf : Supermartingale f ℱ μ) {i j : ι} (hij : i ≤ j) : μ[f j|ℱ i] ≤ᵐ[μ] f i :=
  hf.2.1 i j hij

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