supermartingale — Mathlib

English

For a martingale f, the conditioning of future against past equals the current value in expectation.

Русский

Для мартингейла f условное ожидание будущего относительно прошлого сравняется с текущим значением.

LaTeX

$$$\\forall i \\le j: \\operatorname{condExp}(\\mathcal{F}_i, \\mu, f(j)) = f(i)\\; a.e.$$$

Lean4

theorem supermartingale [Preorder E] (hf : Martingale f ℱ μ) : Supermartingale f ℱ μ :=
  ⟨hf.1, fun i j hij => (hf.2 i j hij).le, fun i => hf.integrable i⟩

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