ae_le_condExp — Mathlib

English

For a Submartingale, for i ≤ j, f_i is almost surely bounded above by the conditional expectation of f_j given ℱ_i, almost surely.

Русский

Для субмартингала, при i ≤ j, f_i почти surely не превосходит условное ожидание f_j по ℱ_i.

LaTeX

$$$\mathrm{Submartingale}(f,\mathcal{F},\mu) \Rightarrow \forall \{i,j\}, i \le j \Rightarrow (\mu\text{-a.e.})\; f_i \le \mathrm{condExp}(\mathcal{F}.seq(i))\mu(f_j)$$$

Lean4

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

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