English
A family of integrable functions f: ι → Ω → E is a martingale with respect to a filtration ℱ if it is adapted and for all i ≤ j, μ[f j | ℱ i] equals f i almost surely.
Русский
Семейство интегрируемых функций f: ι → Ω → E является мартингейлом относительно фильтрации ℱ, если оно адаптировано и для любых i ≤ j условное математическое ожидание μ[f j | ℱ i] равно f i почти наверняка.
LaTeX
$$$\\text{Martingale}(f, \\mathcal{F}, \\mu) := \\text{Adapted }\\mathcal{F} \\\\text{f} \\land \\forall i \\ j, i \\le j \\Rightarrow \\mu[f(j) | \\mathcal{F}(i)] =_{\\mu}^{ae} f(i)$$$
Lean4
/-- A family of functions `f : ι → Ω → E` is a martingale with respect to a filtration `ℱ` if `f`
is adapted with respect to `ℱ` and for all `i ≤ j`, `μ[f j | ℱ i] =ᵐ[μ] f i`. -/
def Martingale (f : ι → Ω → E) (ℱ : Filtration ι m0) (μ : Measure Ω) : Prop :=
Adapted ℱ f ∧ ∀ i j, i ≤ j → μ[f j|ℱ i] =ᵐ[μ] f i
