English
Let μ be finite. If f is Adapted to 𝒢 and for all i, f_i equals the conditional expectation of f_{i+1} given 𝒢_i almost surely, then f is a Martingale.
Русский
Пусть μ конечная; если f адаптирован к 𝒢 и для всех i выполняется f_i = ⟪f_{i+1}⟫_{𝒢_i} почти наверняка, то f — мартингал.
LaTeX
$$$[IsFiniteMeasure \\ μ] \\Rightarrow (Adapted 𝒢 f) \\land (\\forall i, f_i =^{\\text{ae}}_{μ} \\mathbb{E}[f_{i+1} | \\mathcal{G}_i]) \\Rightarrow \\text{Martingale}(f, 𝒢, μ).$$$
Lean4
theorem martingale_nat [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ} (hadp : Adapted 𝒢 f) (hint : ∀ i, Integrable (f i) μ)
(hf : ∀ i, f i =ᵐ[μ] μ[f (i + 1)|𝒢 i]) : Martingale f 𝒢 μ :=
martingale_iff.2
⟨supermartingale_nat hadp hint fun i => (hf i).symm.le, submartingale_nat hadp hint fun i => (hf i).le⟩
