martingale_zero — Mathlib

English

The zero process f(i) = 0 is a martingale with respect to any filtration and finite measure μ.

Русский

Нулевая последовательность f(i) = 0 является мартингалем относительно любой фильтрации и конечной меры μ.

LaTeX

$$$\\text{Martingale}(0, \\mathcal{F}, \\mu)$$$

Lean4

theorem martingale_zero (ℱ : Filtration ι m0) (μ : Measure Ω) : Martingale (0 : ι → Ω → E) ℱ μ :=
  ⟨adapted_zero E ℱ, fun i j _ => by simp⟩

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