English
Let μ be finite. If f: ℕ → Ω → ℝ is Adapted to 𝒢, integrable, and for all i we have μ[f_{i+1} − f_i | 𝒢_i] =ᵐ[μ] 0, then f is a Martingale.
Русский
Пусть μ конечна. Если f адаптирован к 𝒢, интегрируем и для всех i μ[f_{i+1} − f_i | 𝒢_i] = 0 почти наверняка, то f — мартингал.
LaTeX
$$$[IsFiniteMeasure \\ μ] \\Rightarrow (Adapted 𝒢 f) \\land (\\forall i, Integrable (f_i) \\ μ) \\land (\\forall i, μ[f_{i+1} - f_i | 𝒢_i] =^{ae}_{μ} 0) \\Rightarrow \\text{Martingale}(f, 𝒢, μ).$$$
Lean4
theorem martingale_of_condExp_sub_eq_zero_nat [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ} (hadp : Adapted 𝒢 f)
(hint : ∀ i, Integrable (f i) μ) (hf : ∀ i, μ[f (i + 1) - f i|𝒢 i] =ᵐ[μ] 0) : Martingale f 𝒢 μ :=
by
refine
martingale_iff.2
⟨supermartingale_of_condExp_sub_nonneg_nat hadp hint fun i => ?_,
submartingale_of_condExp_sub_nonneg_nat hadp hint fun i => (hf i).symm.le⟩
rw [← neg_sub]
refine (EventuallyEq.trans ?_ (condExp_neg ..).symm).le
filter_upwards [hf i] with x hx
simpa only [Pi.zero_apply, Pi.neg_apply, zero_eq_neg]
-- Note that one cannot use `Submartingale.zero_le_of_predictable` to prove the other two
-- corresponding lemmas without imposing more restrictions to the ordering of `E`
