martingale_iff — Mathlib

English

For a martingale, the conditional expectation of f j given ℱ i equals f i a.e. whenever i ≤ j.

Русский

Для мартингайла условное ожидание f(j) по ℱ(i) равно f(i) почти наверняка при i ≤ j.

LaTeX

$$$\\forall i \\le j: \\mu[f(j) | \\mathcal{F}_i] =_{ae} f(i)$$$

Lean4

theorem martingale_iff [PartialOrder E] : Martingale f ℱ μ ↔ Supermartingale f ℱ μ ∧ Submartingale f ℱ μ :=
  ⟨fun hf => ⟨hf.supermartingale, hf.submartingale⟩, fun ⟨hf₁, hf₂⟩ =>
    ⟨hf₁.1, fun i j hij => (hf₁.2.1 i j hij).antisymm (hf₂.2.1 i j hij)⟩⟩

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